@MISC{JS90, author = "Geraint Jones and Mary Sheeran", title = "Circuit design in {Ruby}", howpublished = "Lecture notes on Ruby from a summer school in Lyngby, Denmark.", month = sep, year = "1990", } @INCOLLECTION{Fou96, AUTHOR = {Michael P. Fourman}, TITLE = {Proof and design}, BOOKTITLE = {Deductive Program Design}, PAGES = {397-439}, PUBLISHER = {Springer}, YEAR = {1996}, EDITOR = {Manfred Broy}, VOLUME = {152}, SERIES = {NATO Advanced Science Institute, Series F: Computer and System Sciences}, ADDRESS = {Marktoberdorf Germany}, MONTH = {July}, NOTE = {Proceedings of the NATO Advanced Study Institute on Deductive Program Design, also available as LFCS report ECS-LFCS-95-319} } @Article{Bac78, author = "John Backus", title = "Can Programming Be Liberated From the {von Neumann} Style? {A} Functional Style and its Algebra of Programs", journal = "Communications of the ACM", volume = "21", number = "8", pages = "613--641", month = aug, year = "1978", CODEN = "CACMA2", ISSN = "0001-0782" } @InProceedings{She84, author = "Mary Sheeran", title = "mu{FP}, {A} Language for {VLSI} Design", booktitle = "Conference Record of the 1984 {ACM} Symposium on Lisp and Functional Programming", organization = "ACM", publisher = "ACM", month = aug, year = "1984", pages = "104--112" } @Article{MW97, title = "Otter --- {The} {CADE-13} Competition Incarnations", author = "William McCune and Larry Wos", journal = "Journal of Automated Reasoning", pages = "211--220", month = apr, year = "1997", volume = "18", number = "2", } @Article{Tam97, title = "Gandalf", author = "Tanel Tammet", journal = "Journal of Automated Reasoning", pages = "199--204", month = apr, year = "1997", volume = "18", number = "2", } @Article{BCSS99, author = "Per Bjesse and Koen Claessen and Mary Sheeran and Satnam Singh", title = "{Lava}: Hardware Design in {Haskell}", journal = "ACM SIG{\-}PLAN Notices", volume = "34", number = "1", pages = "174--184", month = jan, year = "1999", CODEN = "SINODQ", ISSN = "0362-1340", affiliation = "Chalmers University; Xilinx", } @InProceedings{DR04, title = "Derivation of a Logarithmic Time Carry Lookahead Addition Circuit", author = {John O'Donnell and Gudula R\"{u}nger}, booktitle = "Journal of Functional Programming", volume = "14, number~6", page = "697--713", publisher = "Cambridge University Press", year = "2004"} @InProceedings{OD02, title = "Overview of {Hydra}: {A} concurrent language for synchronous digital circuit design", author = "John O'Donnell", booktitle = "Proceedings of the 16th International Parallel and Distributed Processing Symposium", publisher = "IEEE Computer Society Press", year = "2002"} @InProceedings{OD87, author = {John O'Donnell}, title = {Hardware description with recursion equations}, booktitle = {Proceedings of the IFIP 8th International Symposium on Computer Hardware Description Languages and their Applications}, pages = {363--382}, year = 1987, address = {Amsterdam}, month = {April}, publisher = {North-Holland} } @InProceedings{Blu01, author = {Christian Blumenr\"{o}hr}, title = {A formal approach to specify and synthesize at the system level}, booktitle = {GI Workshop Modellierung und Verifikation von Systemen}, pages = {11--20}, year = 1999, address = {Braunschweig, Germany}, publisher = {Shaker-Verlag} } @InProceedings{BS99, author = {Christian Blumenr\"{o}hr and Viktor Sabelfeld}, title = {Formal synthesis at the algorithmic level}, editor = {Laurence Pierre and Thomas Kropf}, booktitle = {Correct Hardware Design and Verification Methods, 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME '99}, address = {Bad Herrenalb, Germany}, month = {September}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {1703}, year = {1999}, pages = {187--201}} @InProceedings{Gropius1, author = {Christian Blumenr\"{o}hr and Dirk Eisenbiegler}, title = {Performing High-Level Synthesis via Program Transformations within a Theorem Prover}, booktitle = {Proceedings of the Digital System Design Workshop at the Euromicro 98 Conference, V\"{a}steras, Sweden}, pages = {34-37}, year = 1998, address = {Universit\"{a}t Karlsruhe, Institut f\"{u}r Rechnerentwurf und Fehlertoleranz}, } @InProceedings{Gropius2, author = {V. Sabelfeld, C. Blumenr\"{o}hr and K. Kapp}, title = {Semantics and Transformations in Formal Synthesis at System Level}, booktitle = {Perspectives of System Informatics, 4th International Andrei Ershov Memorial Conference, Novosibirsk, Russia}, editor = {Dines Bjorner and Manfred Broy and Alexandre Zamulin}, pages = {149-156}, year = 2001, address = {Universit\"{a}t Karlsruhe, Institut f\"{u}r Rechnerentwurf und Fehlertoleranz}, publisher = {Springer-Verlag}, series = {LNCS 2244}, } @INPROCEEDINGS{Fou89, AUTHOR = {Simon Finn and Michael P. Fourman and Michael Francis and Robert Harris}, TITLE = {Formal system design---interactive synthesis based on computer-assisted formal reasoning}, BOOKTITLE = {IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Volume 1}, YEAR = {1989}, MONTH = {November}, EDITOR = {Luc Claesen}, PAGES = {97--110}, PUBLISHER = {Elsevier Science Publishers, B.V. North-Holland, Amsterdam}, ADDRESS = {Houthalen, Belgium} } @InProceedings{HLD89, author = "F.K. Hanna and M. Longley and N. Daeche", booktitle = "Applied Formal Methods for Correct {VLSI} Design", editor = "{L. Claesen}", publisher = "North-Holland", pages = "153-170", title = "Formal Synthesis of Digital Systems", year = "1989" } @inproceedings{ hanna92, author = "{F.K. Hanna} and {N. Daeche} and {G. Howells}", title = "Implementation of the {Veritas Design Logic}", booktitle = "Proceedings of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience", publisher = "North-Holland", address = "Nijmegen", editor = "{V. Stavridon} and {T.F. Melham} and {R.T. Boute}", pages = "77--94", year = "1992" } @InProceedings{CP02, title = "An Embedded Language Framework for Hardware Compilation", author = "Koen Claessen and Gordon Pace", booktitle = "Designing Correct Circuits 2002 (DCC 2002)", address = "Grenoble, France", year = "2002" } @Book{Jon03, editor = "Simon Peyton Jones", title = "Haskell 98 Language and Libraries -- The Revised Report", publisher = "Cambridge University Press", address = "Cambridge, England", year = "2003" } @InProceedings{VB01, author = "Miroslav N. Velev and Randal E. Bryant", title = "{EVC}: {A} Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations", booktitle = "Proceedings of the 13th International Conference on Computer Aided Verification (CAV'01)", address = "Paris, France", month = "July", volume = "2102", pages = "235--240", year = "2001" } @InProceedings{GN02, author = "E. Goldberg and Y. Novikov", title = "{BerkMin}: {A} Fast and Robust {SAT}-Solver", booktitle = "Proceedings of the Design, Automation, and Test in Europe (DATE'02)", month = "March", address = "Paris, France", year = "2002", pages = "142--149" } @InProceedings{BD94, address = "Stanford, California, USA", author = "J. R. Burch and D. L. Dill", booktitle = "Proceedings of the 6th International Conference on Computer Aided Verification (CAV'94)", month = "June", pages = "68--80", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", title = "Automatic Verification of Pipelined Microprocessors Control", volume = "818", year = "1994" } @InProceedings{Arv03, author = "Arvind", title = "Bluespec: A language for hardware design, simulation, synthesis and verification", booktitle = "Proceedings of the First ACM and IEEE International Conference on Formal Methods and Models for Co-design (MEMOCODE'03)", year = "2003", month = "June", pages = "249--251", address = "Mont Saint-Michel, France", note = "Invited Talk" } @InProceedings{STG03, author = "Sandeep Shukla and Jean-Pierre Talpin and Rajesh K. Gupta", title = "Message from the chairs", booktitle = "Proceedings of the First ACM and IEEE International Conference on Formal Methods and Models for Co-design (MEMOCODE'03)", year = "2003", month = "June", pages = "viii--ix", address = "Mont Saint-Michel, France" } @Article{CDE+02, author = "M. Clavel and F. Dur{\'a}n and S. Eker and P. Lincoln and N. Mart{\'\i}-Oliet and J. Meseguer and J. F. Quesada", title = "{Maude}: specification and programming in rewriting logic", journal = "Theoretical Computer Science", volume = "285", number = "2", pages = "187--243", year = "2002" } @Article{Mes92, author = "Jos\'e Meseguer", title = "Conditional rewriting logic as a unified model of concurrency", journal = "Theoretical Computer Science", volume = "96", number = "1", pages = "73--155", year = "1992" } @InProceedings{Mes03, author = "Jos\'e Meseguer", title = "Executable Computational Logics: Combining Formal Methods and Programming Language Based System Design", booktitle = "Proceedings of the First ACM and IEEE International Conference on Formal Methods and Models for Co-design (MEMOCODE'03)", year = "2003", month = "June", pages = "3--9", address = "Mont Saint-Michel, France", note = "Invited Talk" } @InProceedings{SV03, author = "Sudarshan K. Srinivasan and Miroslav N. Velev", title = "Formal Verification of an {Intel} {XScale} Processor Model with Scoreboarding, Specialized Execution Pipelines, and Imprecise Data-Memory Exceptions", booktitle = "Proceedings of the First ACM and IEEE International Conference on Formal Methods and Models for Co-design (MEMOCODE'03)", year = "2003", month = "June", pages = "65-74", address = "Mont Saint-Michel, France" } @Book{Mos86, author = "Ben C. Moszkowski", title = "Executing temporal logic programs", publisher = "Cambridge University Press", address = "Cambridge, England", year = "1986" } @InCollection{Gor86, author = "Michael J. C. Gordon", booktitle = "Formal Aspects of {VLSI} Design", editor = "G. J. Milne and P.A. Subrahmanyam", pages = "153--177", publisher = "North-Holland", remark = "Technical Report 77", title = "Why Higher-Order Logic is a Good Formalism for Specifying and Verifying Hardware", year = "1986" } @phdthesis{Sha02, title = "Higher-Level Hardware Synthesis", author = "Richard Sharp", school = "University of Cambridge, the Computer Laboratory", year = "2002", address = "Cambridge, England" } @Book{Mel93, author = "Thomas F. Melham", title = "Higher Order Logic and Hardware Verification", publisher = "Cambridge University Press", address = "Cambridge, England", note = "Cambridge Tracts in Theoretical Computer Science 31", year = "1993" } @manual{HOL02, title = "The HOL System Tutorial", month = "June", year = "2002", key = "HOLtutorial" } @mastersthesis{Iyo00, author = "Juliano Iyoda", title = "{ParTS} - {A} tool for hardware/software partitioning", school = "Universidade Federal de Pernambuco", year = "2000", address = "Brazil", note = "In~Portuguese" } @techreport{IJ01a, author = "Juliano Iyoda and He Jifeng", title = "Towards an Algebraic Synthesis of {Verilog}", institution = "UNU/IIST", year = "2001", number = "218", address = "Macao SAR, P. R. China" } @techreport{Johnson90, author = "Steven D. Johnson and Bhaskar Bose", title = "{DDD -- A System for Mechanized Digital Design Derivation}", institution = "Indiana University", year = "1990", number = "TR323", address = "IU Computer Science Department" } @techreport{Fox01, author = "Anthony C. J. Fox", title = "An Algebraic Framework for Modelling and Verifying Microprocessors using {HOL}", institution = "The Computer Laboratory, University of Cambridge", number = "512", year = "2001", month = "March", address = "England" } @misc{FoxWord32, author = "Anthony C. J. Fox", title = "{HOL $n$-bit word Library}", institution = "The Computer Laboratory, University of Cambridge", year = "2004", month = "February", note = {Documentation available with the HOL4 system} } @techreport{Fox02, author = "Anthony C. J. Fox", title = "Formal verification of the {ARM6} micro-architecture", institution = "The Computer Laboratory, University of Cambridge", number = "548", year = "2002", month = "November", address = "England" } @Book{GM93, editor = "Michael J. C. Gordon and Thomas F. Melham", publisher = "Cambridge University Press", title = "Introduction to {HOL}: {A} theorem proving environment for higher order logic", year = "1993", note = "HOL4 website: http:/$\!$/hol.sourceforge.net" } @inproceedings{Gor02, title = "Using {HOL} to study {Sugar} 2.0 semantics", author = "Michael J. C. Gordon", booktitle = "Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002)", year = "2002", month = "August", address = "Hampton, Virginia, U.S.A." } @inproceedings{MS01a, title = "Hardware Synthesis Using {SAFL} and Application to Processor Design", author = "Alan Mycroft and Richard Sharp", booktitle = "Proceedings of the 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'01)", year = "2001", address = "Livingston, Scotland", month = "September", publisher = "Springer Verlag", note = "Invited Talk. LNCS Vol. 2144" } @inproceedings{MS01b, title = "Hardware/software co-design using functional languages", author = "Alan Mycroft and Richard Sharp", booktitle = "Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01)", note = "LNCS Vol. 2031", publisher = "Springer-Verlag", pages = "236--251", address = "Genova, Italy", month = "April", year = "2001" } @inproceedings{IJ01b, title = "Towards an Algebraic Synthesis of {Verilog}", author = "Juliano Iyoda and He Jifeng", pages = "15--21", booktitle = "Proceedings of the International Conference on Engineering of Reconfigurable Systems and Algorithms", year = "2001", address = "Las Vegas, Nevada, USA" } @techreport{IJ01c, author = "Juliano Iyoda and He Jifeng", title = "A {Prolog} Prototype for the Synthesis of {Verilog}", institution = "UNU/IIST", year = "2001", number = "237", address = "Macao SAR, P. R. China" } @Book{SS94, author = "Leon Sterling and Ehud Shapiro", title = "The Art of Prolog", edition = "Second", publisher = "The MIT Press", address = "Cambridge, Mass.", year = "1994" } @book{TM98, author = "Donald E. Thomas and Philip R. Moorby", title = "The {Verilog} Hardware Description Language", publisher = "Kluwer Academic Publishers", edition = "fourth", year = "1998" } @inproceedings{HX00, author = "He Jifeng and Xu Qiwen", title = "An Operational Semantics of a Simulator Algorithm", booktitle = "Proceedings of the 2000 International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'2000)", address = "Las Vegas, Nevada, USA", month = "June 26-29", year = "2000" } @techreport{LH00a, author = "Li YongJian and He Jifeng", title = "Towards Unifying Theories of {Verilog} -- {Part} 1: Operational Semantics, Bisimulation and Observation Equivalence", institution = "UNU/IIST", year = "2000", number = "217", address = "Macao SAR, China" } @techreport{LH00b, author = "Li YongJian and He Jifeng", title = "Towards Unifying Theories of {Verilog} -- {Part} 2: The Algebraic Laws of {Verilog}", institution = "UNU/IIST", year = "2000", number = "217", address = "Macao SAR, China" } @phdthesis{Pac98, title = "Hardware Design Based on Verilog HDL", author = "Gordon J. Pace", school = "University of Oxford", year = "1998", address = "England", note = "Computing {L}aboratory" } @unpublished{Gor97, title = "Synthesizable {Verilog} --- syntax and semantics", author = "Mike Gordon", note = "Manuscript. VFE Project. University of Cambridge Computer Laboratory", year = "1997" } @inproceedings{Gor95, title = "The Semantic Challenge of {Verilog} {HDL}", author = "Mike Gordon", pages = "136--145", booktitle = "Proceedings of Tenth Annual {IEEE} Symposium on Logic in Computer Science", year = "1995", address = "San Diego, California", organization = "IEEE Computer Society Press" } @book{HJ98, author = "C. A. R. Hoare and He Jifeng", title = "Unifying Theories of Programming", publisher = "Prentice Hall International Series in Computer Science", year = "1998" } @book{IEEE-1364-1996, author = "IEEE", title = "{IEEE} Standard Hardware Description Language Based on the Verilog %$^{\textstyle{\scriptsize{\textregistered}}}$ Hardware Description Language", publisher = "The Institute of Electrical and Electronic Engineers, Inc.", address = "New York, NY", year = "1996" } @book{IEEE-P1364.1-1999, author = "IEEE", title = "{IEEE} P1364.1/D1.4 Draft Standard for Verilog %$^{\textstyle{\scriptsize{\textregistered}}}$ Register Transfer Level Synthesis", publisher = "The Institute of Electrical and Electronic Engineers, Inc.", address = "New York, NY", year = "1999" } @booklet{XNF6.1, author = "{Xilinx, Inc.}", title = "{Xilinx Netlist Format (XNF) Specification}", address = "{http://www.xilinx.com}", year = "1995", note = "Version 6.1" } @inproceedings{CGH+93, title = "A Formal Specification Model for Hardware/Software Codesign", author = "Massimiliano Chiodo and Paolo Giusto and Harry Hsieh and Attila Jurecska and Luciano Lavagno and Alberto L. Sangiovanni-Vincentelli", month = "October", year = "1993", booktitle = "Proceedings of International Workshop on Hardware-Software Codesign" } @InProceedings{SVSL00, author = "Alberto L. Sangiovanni-Vincentelli and Marco Sgroi and Luciano Lavagno", title = "Formal Models for Communication-Based Design", booktitle = "Proceedings of the 11th International Conference on Concurrency Theory (CONCUR'00)", publisher = "LNCS, Springer-Verlag", month = "August", year = "2000" } @InProceedings{NYBJ01, author = "Gabriela Nicolescu and Sungjoo Yoo and Aimen Bouchhima and Ahmed A. Jerraya", title = "Validation in a Component-Based Design Flow for Multicore {SoC}", pages = "162--167", booktitle = "Proceedings of the International Symposium on Systems Synthesis", address = "Kyoto, Japan", month = "October", year = "2002" } @InProceedings{BYJ01, author = "Iuliana Bacivarov and Sungjoo Yoo and Ahmed A. Jerraya", title = "Timed {HW}-{SW} Cosimulation Using Native Execution of {OS} and Application {SW}", pages = "195--200", booktitle = "Proceedings of the Seventh Annual IEEE International Workshop on High Level Design Validation and Test", address = "Cannes, France", year = "2001" } @InProceedings{LSV96, author = "Edward A. Lee and Alberto L. Sangiovanni-Vincetelli", title = "Comparing Models of Computation", pages = "234--243", booktitle = "Proceedings of the International Conference on Computer-Aided Design (ICCAD '96)", address = "San Jose, CA, USA", year = "1996" } @inproceedings{BPSV01a, author = {Jerry R. Burch and Roberto Passerone and Alberto L. Sangiovanni-Vincentelli}, title = {Overcoming Heterophobia: Modeling Concurrency in Heterogeneous Systems}, booktitle = {Proceedings of the second International Conference on Application of Concurrency to System Design}, month = {June}, address = {Newcastle upon Type, England}, year = {2001} } * @inproceedings{BPSV01b, author = {Jerry R. Burch and Roberto Passerone and Alberto L. Sangiovanni-Vincentelli}, title = {Using Multiple Levels of Abstractions in Embedded Software Design}, booktitle = {Proceedings of the first International Workshop on Embedded Software}, month = {October}, address = {Tahoe City, California}, year = {2001} } @inproceedings{ZC01, title = "Voice Over {IP}: {Correct} Hardware/Software Co-Design", author = "Hussein Zedan and Antonio Cau", booktitle = "8th IEEE Workshop on Future Trends of Distributed Computing Systems (FTDCS'01)", pages = "194--201", year = "2001", month = "October", address = "Bologna, Italy" } @article{SLSV00, author = {Marco Sgroi and Luciano Lavagno and Alberto L. Sangiovanni-Vincentelli}, title = {Formal Models for Embedded System Design}, journal = "IEEE Design and Test of Computers", volume = {17}, number = {2}, pages = {14-27}, month = {June}, year = {2000} } @article{BY96, author = "Robert S. Boyer and Yuan Yu", title = "Automated proofs of object code for a widely used microprocessor", journal = "Journal of the ACM", volume = "43", number = "1", pages = "166--192", year = "1996" } @incollection{MP81, author = "Zohar Manna and Amir Pnueli", booktitle = "The Correctness Problem in Computer Science", chapter = "5", editor = "R. S. Boyer and J. Strother Moore", pages = "215--273", publisher = "Academic Press, London", title = "Temporal Verification of Concurrent Programs: the temporal Framework for Concurrent Programs", year = "1981" } @inproceedings{slind:wfrec, AUTHOR = {Konrad Slind}, TITLE = {Function Definition in Higher Order Logic}, BOOKTITLE = {Theorem Proving in Higher Order Logics}, ADDRESS = {Turku, Finland}, MONTH = {August}, YEAR = 1996, PUBLISHER = {Springer-Verlag}, SERIES = {Lecture Notes in Computer Science}, NUMBER = {1125}, PAGES = {381--398} } @unpublished{AES, AUTHOR = {United States National Institute of Standards and Technology}, TITLE = {{A}dvanced {E}ncryption {S}tandard}, YEAR = 2001, NOTE = "" } @inproceedings{slind:aes, editor = {V. A Carreno and C. A. Munoz and S. Tahar}, AUTHOR = {Konrad Slind}, TITLE = {A Verification of {R}ijndael in {HOL}}, booktitle = {Supplementary Proceedings of TPHOLs 2002}, series = {NASA Conference Proceedings}, number = {CP-2002-211736}, MONTH = {August}, YEAR = 2002 } @ARTICLE{paulson83, author = {Lawrence C. Paulson}, title = {A Higher-Order Implementation of Rewriting}, journal = {Science of Computer Programming}, year = {1983}, volume = {3}, pages = {119-149}, } @inproceedings{TEA, author={David Wheeler and Roger Needham}, title={{TEA}, a tiny encryption algorithm}, booktitle={Fast Software Encryption: Second International Workshop}, year=1999, publisher={Springer Verlag}, series="LNCS", volume=1008, pages="363--366"} @article{DBLP:journals/fmsd/BrockH97, author = {Bishop Brock and Warren A. Hunt Jr.}, title = {The {DUAL-EVAL} Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor.}, journal = {Formal Methods in System Design}, volume = {11}, number = {1}, year = {1997}, pages = {71-104}, bibsource = {DBLP, http://dblp.uni-trier.de} } @misc{CC, key = "Common Criteria", title = "{Common Criteria for Information Security Evaluation}", note = "Part 3: Security Assurance Requirements, \url{http://niap.nist.gov/cc-scheme/cc_docs/cc_v22_part3.pdf}", year = "2004" } @inproceedings{kumar96formal, author = "{R. Kumar} and {C. Blumenroehr} and {D. Eisenbiegler} and {D. Schmid}", title = "Formal Synthesis in circuit design-{A} Classification and survey", booktitle = "First international conference on formal methods in computer-aided design", volume = "1166", publisher = "Springer Verlag", address = "Palo Alto, CA, USA", editor = "{M. Srivas} and {A. Camilleri}", pages = "294--299", year = "1996", url = "citeseer.ist.psu.edu/kumar96formal.html" } @article{hauck93asynchronous, author = "Scott Hauck", journal = "Proceedings of the IEEE", title = "Asynchronous Design Methodologies: An Overview", number = "1", volume = "83", year = "1995", pages = "69--93", url = "citeseer.ist.psu.edu/17380.html" } @book{KeesvanBerkel93, author = {Kees van Berkel}, title = {Handshake circuits: an asynchronous architecture for VLSI programming}, year = {1993}, isbn = {0-521-45254-6}, publisher = {Cambridge University Press}, address = {New York, NY, USA}, } @article{page96constructing, author = "I. Page", title = "Constructing hardware-software systems from a single description", journal = "Journal of VLSI Signal Processing", volume ="12", number = "1", pages = "87--107", year = "1996", note = "{\url{citeseer.ist.psu.edu/page96constructing.html}}" } @inproceedings{Sheeran84, author = {Mary Sheeran}, title = "{$\mu$FP, A Language for VLSI Design}", booktitle = {Proceedings of the ACM Symposium on LISP and Functional Programming}, publisher = "ACM Press, Austin, Texas", year = {1984}, pages = {104-112}, bibsource = {DBLP, http://dblp.uni-trier.de}} @inproceedings{jones91relations, author = "G. Jones and M. Sheeran", title = "Relations and refinement in circuit design", booktitle = "BCS FACS Workshop on Refinement", editor = "C. Morgan", publisher ="Springer-Verlag", year = "1991", url = "citeseer.ist.psu.edu/133448.html" } @inproceedings{Ruby, author = "G. Jones and M. Sheeran", title = "{Circuit design in Ruby}", booktitle = "Formal Methods for VLSI Design", editor = "J. Staunstrup", publisher ="Elsevier Science Publications, North-Holland", pages = "13--70", year = "1990"}