@Book{AptOlderog91, author = "K. R. Apt and E.-R. Olderog", title = "Verification of sequential and concurrent programs", publisher = "Springer-Verlag", address = "New York, Berlin", year = "1991", } @book{coqart, title="Interactive Theorem Proving and Program Development--- Coq'Art: The Calculus of Inductive Constructions", author="Bertot, Y. and Cast\'eran, P.", publisher=springer, year={2004}, series="Texts in Theoretical Computer Science"} @book{book:appel, author = {Andrew W. Appel}, title = {Modern compiler implementation in Java}, year = {1998}, isbn = {0-521-58388-8}, publisher = {Cambridge University Press}, address = {New York, NY, USA}, } @Article{vlisp, author = "J. D. Guttman and M. Wand", title = "Special Issue on {VLISP}", journal = "Lisp and Symbolic Computation", volume = "8", number = "1/2", month = mar, year = "1995"} @Book{CGP:book, author = "E.M. Clarke and O. Grumberg and D.A. Peled", title = "Model Checking", publisher = "The {MIT} Press", year = "1999", address = "Cambridge, Massachusetts", isbn_issn = "0262032708", } @book{che:book, title={Java Card for Smart Cards: Architecture and Programmer's Guide}, author={Z. Chen}, series={The Java Series}, publisher={O'Reilly}, year={2000}} @Book{dij:book, author = "E. W. Dijkstra", title = "A Discipline of Programming", publisher = "Prentice-Hall", year = "1976"} @Book{mil+:smlrev, author = "R. Milner and M. Tofte and R. Harper and D. MacQueen", year = "1997", title = "The {Definition} of {Standard ML} (Revised)", publisher = "The MIT Press"} @Book{cmp:caml, title={{D{\'e}veloppement d'applications avec Objective Caml}}, author={E. Chailloux and P. Manoury and B. Pagano}, publisher={O'Reilly}, year={2000}} @Book{pau:ml, author = "L. C. Paulson", title = "{ML} for the Working Programmer", publisher = cup, year = "1996"} @book{bir:haskell, author={R. Bird}, title={Introduction to Functional Programming using Haskell}, edition=2, publisher=ph, year={1998}} @book{CM98:caml, title={The functional approach to programming}, author={G. Cousineau and M. Mauny}, publisher=cup, year={1998}} @Book{schneier:book, author = "B. Schneier", title = "Applied Cryptography (Second Edition)", publisher = "John Wiley \& Sons", year = "1996", } @book{SW:pi , author = {Sangiorgi, D. and Walker, D.}, publisher = {{C}ambridge {U}niversity {P}ress}, title = {The $\pi$-calculus: a {T}heory of {M}obile {P}rocesses}, year = {2001} } %%%%%%%%%%%%%%%%%%%%%%%%% COLLECTIONS %%%%%%%%%%%%%%%%%%%%%%%%%%% @incollection{GWB:ad, author={J. Giesl and C. Walther and J. Brauburger}, title={Termination Analysis for Functional Programs}, booktitle={Automated Deduction - A Basis for Applications}, volume=3, editor={W. Bibel and P. Schmitt}, pages={135--164}, series={Applied Logic Series}, publisher=kluwer, year={1998}} @InCollection{petera78:czf, author = "P. Aczel", title = "{The Type Theoretic Interpretation of Constructive Set Theory}", editor = "A. MacIntyre and A. Pacholski and J. Paris", booktitle = "{Proceedings of Logic Colloqium 77}", series = "Studies in Logic and the Foundations of Mathematics", pages = "55--66", publisher = "North-Holland", year = "1978" } @InCollection{petera82:czf, author = "P. Aczel", title = "{The Type Theoretic Interpretation of Constructive Set Theory: Choice Principles}", editor = "A. S. Troelstra and D. van Dalen", booktitle = "{Proceedings L.~E.~J. Brouwer Centenary Symposium}", series = "Studies in Logic and the Foundations of Mathematics", volume = "110", pages = "1--40", publisher = "North-Holland", year = "1982" } @InCollection{petera86:czf, author = "P. Aczel", title = "{The Type Theoretic Interpretation of Constructive Set Theory: Inductive Definitions}", editor = "R. B. Marcus and G. J. W. Dorn and P. Weingartner", booktitle = "Proceedings of Logic, Methodology and Philosphy of Science VII", series = "Studies in Logic and the Foundations of Mathematics", volume = "114", pages = "17--49", publisher = "North-Holland", year = "1986" } @incollection{petera:handbook, author={P. Aczel}, title={An introduction to inductive definitions}, booktitle={Handbook of mathematical logic}, editor={J. Barwise}, year={1977}, publisher="North-Holland", series="Studies in Logic and the Foundations of Mathematics", volume=90, pages={739--782} } @incollection{petera94:logic, author={P. Aczel}, title={Schematic Consequence}, booktitle={What is a logical system?}, editor={D. Gabbay}, year={1994}, publisher=oup } @Book{abr:bbook, author = "J.-R. Abrial", title = "The {B}-Book: Assigning Programs to Meanings", publisher = "Cambridge University Press", year = "1996"} @book{BW:book, author={J.C.M. Baeten and W.P. Weijland}, title={Process Algebra}, publisher={Cambridge University Press}, series={Cambridge Tracts in Theoretical Computer Science}, volume={18}, year={1990}} @incollection{BM:handbook, author={D. Basin and S. Matthews}, title={{Logical Frameworks}}, booktitle={Handbook of Philosophical Logic}, year={2002}, EDITOR = {D. Gabbay and F. Guenthner}, publisher=kluwer, volume=9} @book{beeson:foundation, author = "M. Beeson", title = "{Foundation of Constructive Mathematics}", publisher = "Springer-Verlag", year = 1985 } @incollection{BT98:twentyfive, author={G. Betarte and A. Tasistro}, title={{Extension of Martin-L{\"o}f's type theory with record types and subtyping}}, booktitle={Twenty-five Years of Constructive Type Theory}, publisher=oup, year={1998}, editor={G. Sambin and J. Smith}} @InCollection{BS01:handbook, author = "J. Bradfield and C. Stirling", editor = "J. Bergstra and A. Ponse and S. Smolka", title = "Modal logics and mu-calculi", booktitle = "Handbook of Process Algebra", publisher = "Elsevier, North-Holland", year = "2001", pages = "293--332"} @book{bss:jbook, title={{Java and the Java Virtual Machine - Definition, Verification, Validation}}, author={R. St{\"a}rk and J. Schmid and E. B{\"o}rger}, publisher=springer, year={2001}} @book{BS:asm, title={{Abstract State Machines -- A Method for High-Level System Design and Analysis}}, author={ E. B{\"o}rger and R. St{\"a}rk}, publisher=springer, year={2003}} @InCollection{CM90:lf, author = {Constable, R. and Murthy, C.R.}, title = {Finding Computational Contents in Classical Proofs}, booktitle = {Proceedings of the First Workshop on Logical Frameworks}, publisher = CUP, year = 1990, editor = {Huet, G. and Plotkin, G.}, pages = {341--362} } @Book{DHK:book, editor = {Deursen, A. van and Heering, J. and Klint, P.}, title = {Language Prototyping: an algebraic specification approach}, publisher = {World Scientific}, year = {1996}, series = {{AMAST Series in Computing}} } @InCollection{dyb91:lf, author = "P. Dybjer", title = "Inductive Sets and Families in {M}artin-{L}{\"o}f's Type Theory and Their Set-Theoretic Semantics", editor = "G. Huet and G. Plotkin", booktitle = "Logical Frameworks", publisher = "Cambridge University Press", year = "1991", pages = "280--306"} @InCollection{KW98:ar, author = "T. Kolbe and C. Walther", title = "Proof Analysis, Generalization, and Reuse", booktitle = "Automated Deduction: A Basis for Applications. Volume {II}, Systems and Implementation Techniques", publisher = "Kluwer Academic Publishers", year = "1998", editor = "W. Bibel and P. H. Schmidt" } @InCollection{ML85:mlpl, author = "P. Martin-L{\"{o}}f", editor = "C. A. R. Hoare and J. C. Shepherdson", title = "Constructive Mathematics and Computer Programming", booktitle = "Mathematical Logic and Programming Languages", pages = "167--184", publisher = "Prentice-Hall", year = "1985", } @InCollection{tai68, author={Tait, W. W.}, title={Constructive reasoning}, year={1968}, booktitle={{Proceedings of the Third International Congress in Logic, Methodology and Philosophy of Science}}, pages={185--199}, publisher=nh} @incollection{SP81:pfa, author={M. Sharir and A. Pnueli}, title={Two approaches to Interprocedural Data Flow Analyses}, booktitle={Program Flow Analysis: Theory and Applications}, editor={S. S. Muchnick and N. D. Jones}, year={1981}, publisher=ph} @book{MJ81:pfa, title={Program Flow Analysis: Theory and Applications}, editor={S. S. Muchnick and N. D. Jones}, year={1981}, publisher=ph} @BOOK{DC:book, AUTHOR = {Di Cosmo, R.}, TITLE = {Isomorphisms of types: from $\lambda$-calculus to information retrieval and language design}, SERIES = {Progress in Theoretical Computer Science}, PUBLISHER = {Birkhauser}, YEAR = {1995} } @incollection{eme:handbook, author={E. Emerson}, title={Temporal and modal logic}, booktitle={Handbook of theoretical computer science}, editor={J. van Leeuwen}, year={1990}, publisher=elsevier, volume={B}, pages={995--1072} } @inCollection{gor:hoots, author = {A.D. Gordon}, title = {Operational Equivalences for Untyped and Polymorphic Object Calculi}, pages = {9--54}, editor = {A.D. Gordon and A.M. Pitts}, booktitle = {Higher Order Operational Techniques in Semantics}, publisher = {Cambridge University Press}, year = 1998 } @inCollection{HS00:robin, author = {G. Huet and A. Sa{\"\i}bi}, title = {{Constructive Category Theory}}, pages = {239--275}, editor = {G. Plotkin and C. Stirling and M. Tofte}, booktitle = {{Proof, Language and Interaction---Essays in honour of Robin Milner}}, publisher = {MIT Press}, year = 2000 } @BOOK{bart:book, AUTHOR = "B. Jacobs", TITLE = "{Categorical Logic and Type Theory}", PUBLISHER = "North Holland", SERIES = "Studies in Logic and the Foundations of Mathematics", NUMBER = "141", YEAR = "1999"} @BOOK{JGS:book, AUTHOR = {N. Jones and C. Gomard and P. Sestoft}, TITLE = {Partial Evaluation and Automatic Program Generation}, PUBLISHER = PH, YEAR = 1993 } @inCollection{MHH:hoots, author = {J.~C. Mitchell and M. Hoang and B.~T. Howard}, title = {Labelling Techniques and Typed Fixed-Point Operators}, pages = {137--174}, editor = {A.D. Gordon and A.M. Pitts}, booktitle = {Higher Order Operational Techniques in Semantics}, publisher = {Cambridge University Press}, year = 1998 } @incollection{ML79, author={P. Martin-L{\"o}f}, title={Constructive Mathematics and Computer Programming}, booktitle={Logic, Methodology and Philosophy of Science 6}, pages={153--175}, publisher=nh, year={1982}} @unpublished{mill:book, author={D. Miller}, title={$\lambda$-Progolog: an introduction to the language and its logic}, note={Draft book}, Year={1998}} @Book{sml97, author={R. Milner and M. Tofte and R. Harper and D. MacQueen}, title={The Definition of Standard ML (Revised)}, Publisher={The MIT Press}, Year={1997}} @book{MT93:book, editor={K. Meinke and J.V. Tucker}, title={Many sorted logic and its applications}, publisher={John Wiley and Sons}, year={1993}} @incollection{NM:handbook, title={Higher-Order Logic Programming}, author={G. Nadathur and D. Miller}, booktitle={Handbook of Logics for Artificial Intelligence and Logic Programming}, volume=5, editor={D. Gabbay and C.J. Hogger and J.A. Robinson}, publisher={Clarendon Press}, pages={499--590}, year={1998}} @incollection{NOP00:fsc, author={T. Nipkow and Oheimb, D. von and C. Pusch}, title={{$\mu$Java}: Embedding a Programming Language in a Theorem Prover}, booktitle={Foundations of Secure Computation. Proceedings of the International Summer School Marktoberdorf 1999}, editor={F.L. Bauer and R. Steinbr\"uggen}, publisher={IOS Press}, pages={117--144}, year=2000} @book{PS:book, title={Object-Oriented Type Systems}, author={J. Palsberg and M.I. Schwartzbach}, publisher={John Wiley \& Sons}, year={1994}} @Book{PJ:book, author = "S. {Peyton Jones}", title = "The Implementation of Functional Programming Languages", publisher = "Prentice Hall", year = "1987" } @book{ros:book, title={Theory and Practice of Concurrency}, author={B. Roscoe}, publisher=PH, year=1997} @book{tho:haskell, title={Haskell. The Craft of Functional Programming}, author={S. Thompson}, publisher={Addison-Wesley}, year={1996}} @book{ung:book, author={A. Ungar}, title={Normalization, cut-elimination and the theory of proofs}, publisher={Center for the Study of Language and Information, Stanford, CA.}, series={Lecture Notes}, number={28}, year={1992}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @incollection{thierry90:lacs, author={T. Coquand}, title={{Metamathematical Investigations of a Calculus of Constructions}}, pages={91-122}, booktitle={{Logic and Computer Science}}, editor={P. Odifreddi}, year={1990}, publisher={Academic Press}} @incollection{thierry:clics, author={T. Coquand}, title={Computational Content of Classical Proofs}, year={1997}, booktitle={Proceedings of the {CLICS} Summer School}, editor={P. Dybjer and A. Pitts}, publisher={Cambridge University Presss}, pages={??--??}} @incollection{martin:clics, author={M. Hofmann}, title={Syntax and Semantics of Dependent Types}, year={1997}, booktitle={Proceedings of the {CLICS} Summer School}, editor={P. Dybjer and A. Pitts}, publisher={Cambridge University Presss}, pages={??--??}} @INCOLLECTION{HL91:otrs, AUTHOR = "Huet, G. and L{\'e}vy, J.-J.", TITLE = "Computations in Orthogonal Rewriting Systems, {I} and {II}", BOOKTITLE = "Computational Logic: Essays in honor of Alan Robinson", PUBLISHER = {The MIT Press}, YEAR = 1991, EDITOR = "Lassez, J-L. and Plotkin, G.", PAGES = "395--443"} @incollection{lam80:cur, AUTHOR = "J. Lambek", TITLE = "From $\lambda$-calculus to cartesian closed categories", BOOKTITLE = "To {H}.{B}. {C}urry: Essays on Combinatory Logic, Lambda Calculus and Formalism", EDITOR = "J.R. Hindley and J.P. Seldin", PUBLISHER = "Academic Press", YEAR = 1980, pages={375--402}} @Book{LS:book, author = "J. Lambek and P. Scott", title = "{Introduction to Higher Order Categorial Logic}", publisher = "Cambridge University Press", year = "1986"} @BOOK{mil+:sml, AUTHOR = "R. Milner and M. Tofte and R. Harper", TITLE = "The Definition of Standard {ML}", PUBLISHER = "The MIT Press", YEAR = 1991} @BOOK{thomas:book, AUTHOR = "Th. Streicher", TITLE = "Semantics of Type Theory. Correctness, Completeness and Independence results", PUBLISHER = "Birkh{\"a}user", SERIES = "Progress in Theoretical Computer Science", YEAR = 1991} @InCollection{god:T, author = "K. Godel", title = "On intuitionistic arithmetic and number theory", pages = "75--81", editor = "{M. Davis}", booktitle = "The Undecidable", publisher = "Raven Press", year = "1965", } @book{AC:book, author={M. Abadi and L. Cardelli}, title={A theory of objects}, publisher={Springer-Verlag}, year={1996}} @book{jw80:crs, author={J.W. Klop}, title={Combinatory reduction systems}, institution={CWI, Amsterdam}, year={1980}, number={127}, series={Mathematical Centre Tracts}, publisher={CWI}} @BOOK{GLT:book, AUTHOR = "J.-Y. Girard and Y. Lafont and P. Taylor", TITLE = "Proofs and {T}ypes", PUBLISHER = "Cambridge University Press", YEAR = 1989, SERIES = "Tracts in Theoretical Computer Science", NUMBER = 7} @INCOLLECTION{MG85, AUTHOR = "J. Meseguer and J. Goguen", TITLE = "Initiality, induction and computability", BOOKTITLE = "Algebraic Methods in Semantics", EDITOR = "M. Nivat and J. Reynolds", PUBLISHER = "Cambridge University Press", PAGES = "459--541", YEAR = 1985} @INCOLLECTION{jw:handbook , AUTHOR = {J.W. Klop} , TITLE = {Term-rewriting systems} , BOOKTITLE = {Handbook of Logic in Computer Science} , EDITOR = {S. Abramsky and D. Gabbay and T. Maibaum} , PUBLISHER = {Oxford Science Publications} , CROSSREF = {AGM} , YEAR = 1992 , PAGES = {1-116} , note={Volume 2}} @incollection{GMNS, author={G. Smolka and W. Nutt and J. Goguen and J. Meseguer}, title={Order-Sorted Equational Computation}, editor={H. Ait-Kaci and M. Nivat}, booktitle={Resolution of Equations in Algebraic Structures}, Volume={2: Rewriting techniques}, pages = "299--367", publisher={Academic Press}, year={1989}} @InCollection{constructor, author = "L. Helmink", title = "Goal Directed Proof Construction In Type Theory", booktitle = "Logical Frameworks", publisher = "Cambridge University Press", year = "1991", editor = "G. Huet and G. Plotkin"} @InCollection{jon93:lf, author = "C. Jones", title = "{Completing the Rationals and Metric Spaces in LEGO}", booktitle = "{Logical Environments}", year = "1993", editor = "G. Huet and G. Plotkin", pages = "297--316", publisher = "Cambridge University Press"} @InCollection{deb91:bra, author = "Bruijn, N.G. de", title = "A plea for weaker frameworks", booktitle = "Logical Frameworks", year = "1991", editor = "G. Huet and G. Plotkin", pages = "40--67", publisher = "Cambridge University Press" } @InCollection{thierry91:lf, author = "Coquand, T.", title = "An algorithm for testing conversion in type theory", booktitle = "Logical Frameworks", year = "1991", editor = "G. Huet and G. Plotkin", pages = "255--279", publisher = "Cambridge University Press" } @Book{app:book, author = {Appel, A.}, title = {Compiling with Continuations}, publisher = {Cambridge University Press}, year = 1992 } @Book{appel:compiler, title={Modern Compiler Implementation in Java}, note={2nd Edition}, author={A.W. Appel, with J. Palsberg}, year={2002}, publisher={{Cambridge University Press}}} @incollection{ter:vd, author={J. Terlouw}, title= {Strong normalisation in type systems: a model-theoretical approach}, booktitle={Dirk van Dalen Festschrift}, editors={H. Barendregt and M. Bezem and J.W. Klop}, publisher={University of Utrecht}, pages={161-190}, note={To appear in Annals of Pure and Applied Logic}, year={1993}} @incollection{rez:vd, author={A. Rezus}, title= {Beyond {BHK}}, booktitle={Dirk van Dalen Festschrift}, editors={H. Barendregt and M. Bezem and J.W. Klop}, publisher={University of Utrecht}, pages={114--120}, year={1993}} @BOOK{pra:book , AUTHOR = {Prawitz, D.} , TITLE = {Natural Deduction: A proof theoretical study} , PUBLISHER = {Almquist \& Wiksell} , YEAR = 1965 } @INCOLLECTION{henk:handbook , AUTHOR = {H. Barendregt} , TITLE = {Lambda Calculi with Types} , BOOKTITLE = {Handbook of Logic in Computer Science} , EDITOR = {S. Abramsky and D. Gabbay and T. Maibaum} , PUBLISHER = {Oxford Science Publications} , CROSSREFONLY = {AGM} , YEAR = 1992 , PAGES = {117--309} , note={Volume 2}} @INCOLLECTION{pfe:handbook , AUTHOR = {F. Pfenning} , TITLE = {{Logical Frameworks}} , BOOKTITLE = {Handbook of Automated Reasoning} , PUBLISHER = {Elsevier Publishing} , editor = {A. Robinson and A. Voronkov} , year = 2001 , volume = {II} , pages = {1063-1147}, chapter={17}} @INCOLLECTION{hh:handbook , AUTHOR = {H. Barendregt and H. Geuvers} , TITLE = {Proof Assistants using Dependent Type Systems} , BOOKTITLE = {Handbook of Automated Reasoning} , PUBLISHER = {Elsevier Publishing} , Editor={A. Robinson and A. Voronkov} , YEAR = {2001} ,volume = {II} , pages = {1149-1238} ,chapter={18}} @incollection{dBr:role, crossref={louvain:CH}, author={N.G. de Bruijn}, title= {On the roles of types in mathematics}, pages={27-54}, editor={{P. de Groote}}, booktitle={{The Curry-Howard isomorphism}}, publisher={{Universite catholique de Louvain}}, year={1995}, volume={8}, series={{Cahiers du centre de logique}}} @incollection{vernacular, crossref={automath}, author={N.G. de Bruijn}, title= {The mathematical vernacular, a language for mathematics with typed sets}, booktitle={Selected papers on {Automath}}, pages={865-935}} @incollection{deb:pi, crossref={automath}, author={N.G. de Bruijn}, title= {Some extensions of {A}utomath: the {AUT}-4 family}, booktitle={Selected papers on {Automath}}, pages={283--288}} @incollection{herman:louvain, crossref={louvain:CH}, author={H. Geuvers}, title= {{The Calculus of Constructions and higher-order logic}}, pages={139-192}, editor={{P. de Groote}}, booktitle={{The Curry-Howard isomorphism}}, publisher={{Universite catholique de Louvain}}, year={1995}, volume={8}, series={{Cahiers du centre de logique}}} @incollection{jut, crossref={automath}, author={L.S. van Benthem Jutting}, title={{Checking Landau's ``Grundlagen'' in the {Automath} system. Parts of Chapter 0,1, and 2. (Introduction, Preparation and Translation)}}, pages={701-720}} @incollection{zuc:classical, crossref={automath}, author={J. Zucker}, title={Formalisation of classical mathematics in {Automath}}, pages={127-140}} @incollection{zuc:analysis, crossref={automath}, author={L.S. van Benthem Jutting}, title={A text fragment from Zucker's real analysis}, pages={733-762}} @incollection{Gal:red, author={J. Gallier}, title={{On Girard's \lq\lq candidats de r\'educibilit\'e\rq\rq}}, booktitle={Logic and Computer Science}, editor={P. Odifreddi}, pages={123-203}, year={1990}, publisher={Academic Press}} @INCOLLECTION{howard:iso , AUTHOR = {W.A. Howard} , TITLE = {The formulae-as-types notion of construction} , BOOKTITLE = {Essays on Combinatory Logic, Lambda Calculus and Formalism} , EDITOR = {J.R. Hindley and J.P. Seldin} , PUBLISHER = {Academic Press} , CROSSREF = {curry:book} , YEAR = 1980 , PAGES = {479-490} } @incollection{DJ:handbook, author={N. Dershowitz and J.-P. Jouannaud}, title={Rewrite systems}, editor={J. van Leeuwen}, booktitle={Formal models and semantics. Handbook of Theoretical Computer Science}, volume={B}, pages={243-320}, year={1990}, publisher={Elsevier}} @book{PE93, author={Plasmeijer, M.J. and van Eekelen, M.C.J.D.}, title={Functional Programming and Parallel Graph Rewriting}, publisher={Addison-Wesley Publishing Company}, year={1993}} @Book{luo:book, author = "Z. Luo", title = "{Computation and Reasoning: A Type Theory for Computer Science}", publisher = "Oxford University Press", series = "International Series of Monographs on Computer Science", year = "1994", number = 11 } @book{GM:book, author={C.A. Gunter and J.C. Mitchell}, title={Theoretical Aspects of Object-Oriented Programming: Types, Semantics and Language Design}, publisher={{The MIT Press}}, year={1994}} @book{mel:hol, author={T. Melham}, title={Higher Order Logic and Hardware Verification}, series={Tracts in Theoretical Computer Science}, volume={31}, publisher={Cambridge University Press}, year={199?}} @book{henk:book, author="H. Barendregt", title="The Lambda Calculus: Its Syntax and Semantics", edition="revised", publisher="North-Holland", year=1984, series="Studies in Logic and the Foundations of Mathematics", volume=103 } @book{coh:book, author={P. Cohn}, title={Universal algebra}, publisher={D. Reidel}, series={Mathematics and its Applications}, volume={6}, year={1981}} @Book{hol, title = "Introduction to {HOL}: {A} theorem proving environment for higher-order logic", publisher = "Cambridge University Press", year = "1993", editor = "M.J.C. Gordon and T.F. Melham" } @book{ML:book, author="P. {Martin-L\"of}", title="Intuitionistic Type Theory", publisher="Bibliopolis", address="Naples", year=1984, series="Studies in Proof Theory", volume=1 } @book{NPS:book, author = "B. Nordstr{\"{o}}m and K. Petersson and J. Smith", title = "{Programming in Martin-L{\"{o}}f's Type Theory. An Introduction}", publisher = "Oxford University Press", series= {International Series of Monographs on Computer Science}, number= 7, year = 1990 } @book{Wik87, author={A. Wikstr{\"o}m}, title={Functional Progrmmaming using Standard {ML}}, year={1987}, publisher={Prenctice Hall}, series={Interntional Series in Computer Science}} @book{bis67, author="E. Bishop", title="{Foundations of Constructive Analysis}", publisher="McGraw-Hill", year=1967, } @Book{nqthm, author = "R.S. Boyer and J.S. Moore", title = "A Computational Logic Handbook", publisher = "Academic Press", year = 1988 } @BOOK{nuprl , AUTHOR = "R.L. Constable and S.F. Allen and H.M. Bromley and W.R. Cleaveland and J.F. Cremer and R.W. Harper and D.J. Howe and T.B. Knoblock and N.P. Mendler and P. Panangaden and J.T. Sasaki and S.F. Smith" , TITLE = "Implementing Mathematics with the {N}u{P}rl Development System" , PUBLISHER = "Prentice-Hall" , YEAR = 1986 } @BOOK{maclane , AUTHOR = "S. Mc Lane" , TITLE = "Categories for the Working Mathematician" , PUBLISHER = springer , ADDRESS = "Berlin" , YEAR = {1971} } @BOOK{AGM , EDITOR = {S. Abramsky and D. Gabbay and T. Maibaum} , TITLE = {Handbook of Logic in Computer Science} , PUBLISHER = {Oxford Science Publications} , CROSSREFONLY = 1 , YEAR = 1992} @book{galois, author={I. Stewart}, title={Galois theory}, publisher={Chapman and Hall}, year={1989}, edition={second}} @book{automath , Editor={R. Nederpelt and H. Geuvers and R. de Vrijer} , Title={{Selected Papers on Automath}} , publisher="North-Holland" , year=1994 , series="Studies in Logic and the Foundations of Mathematics" , volume=133 } @book{NN:book , author={F. Nielson and H.R. Nielson} , Title={Two-level functional languages} , publisher=cup , year=1992 , series="Cambridge Tracts In Theoretical Computer Science" , volume=34 } @book{NNH:book, author={F. Nielson and H. R. Nielson and C. Hankin}, title={Principles of Program Analysis}, publisher=springer, year=1999} @book{ontic, author={D.A. McAllester}, title={{ONTIC: A Knowledge Representation System for Mathematics}}, publisher={{MIT} Press}, year={1989}} @book{axiom, author={R.D. Jenks and R.S. Sutor}, title={{AXIOM: The Scientific Computation System}}, publisher=springer, year={1992}} @BOOK{curry:book , EDITOR = {J.R. Hindley and J.P. Seldin} , TITLE = {Essays on Combinatory Logic, Lambda Calculus and Formalism} , PUBLISHER = {Academic Press} , ADDRESS = {London} , YEAR = 1980 , CROSSREFONLY = 1 } @book{RW, author={Whitehead, A.N. and Russell, B.}, title={{Principia Mathematica}}, publisher={Cambridge University Press}, year={1910--1913}, volume={1-3}} @book{louvain:CH, editor={de Groote, P.}, title={{The Curry-Howard isomorphism}}, publisher={{Universite catholique de Louvain}}, year={1995}, volume={8}, series={{Cahiers du centre de logique}}} @InCollection{tur90:miranda, author = {Turner, D.}, title = {An Overview of {M}iranda}, crossref = {tur90:book} } @BOOK{tur90:book , EDITOR = {Turner, D.} , BOOKTITLE = {Research Topics in Functional Programming} , PUBLISHER = {Addison-Wesley} , YEAR = 1990 } @BOOK{PD:book, EDITOR={A.~Pitts and P.~Dybjer}, TITLE={Semantics and Logics of Computation}, PUBLISHER={Cambridge University Press}, SERIES={Publications of the Isaac Newton Institute}, YEAR=1997 } @book{hey:book, title = "Intuitionism, an Introduction", author = "A. Heyting", publisher = "North-Holland", year = 1956 } @book{TvD:book, title = "{Constructivism in Mathematics}", author = "A. S. Troelstra and D. van Dalen", publisher = "North-Holland", year = 1988 } @book{terese:book, title={Term Rewriting Systems}, editor={M. Bezem and J. W. Klop and R. de Vrijer}, series={Cambridge Tracts in Theoretical Computer Science}, publisher=cup, year={2003}} @book{BN:rew, title={Term Rewriting and All That}, publisher=cup, author={F. Baader and T. Nipkow}, year={1998}} @book{pie:book, author={B.C. Pierce}, title="Types and Programming Languages", publisher="The MIT Press", year={2002}} @Book{roe+:book, author = {W.-P. de Roever and F. de Boer and U. Hannemann and J. Hooman and Y. Lakhnech and M. Poel and J. Zwiers}, title = {Concurrency Verification: Introduction to Compositional and Noncompositional Methods}, publisher = {Cambridge University Press}, year = 2001, number = 54, series = {Cambridge Tracts in Theoretical Computer Science}, address = {Cambridge, UK}, month = nov, isbn = {0-521-80608-9} } @book{win:book, author={G. Winskel}, title={The Formal Semantics of Programming Languages}, publisher={MIT Press}, year={1993}} @BOOK{Davis-1982a, AUTHOR = "Martin Davis", TITLE = "Computability and Unsolvability", PUBLISHER = Dover, ADDRESS = NY, YEAR = 1982 } @book{and/bel:1975, author = "Anderson, A. R. and Belnap, N. D.", title = "Entailment. The Logic of Relevance and Necessity, {V}olume~1", Publisher = PUP, Address = "U.S.A.", year = 1975 } @manual{coq-8.1, title = "The Coq Proof Assistant Reference Manual, version 8.1", organization = "Coq development team", year = 2006 }