% bib file (data base) % book, booklet, % proceedings, % inbook % incollection (like LNCS) % A article (in journal or magzine), % conference (inproceedings), % masterthesis, phdthesis, % techreport, % manual, % unpublished (eg, to appear) % misc (others, eg talks with no notes) @string{LNCS = "Lecture Notes in Computer Science"} @ARTICLE(burgog:clear80, AUTHOR = "Burstall, R. and Goguen, J.", TITLE = "The Semantics of {Clear}, a Specification Language", JOURNAL = LNCS, VOLUME = "86", NUMBER = "", PAGES = "", YEAR = "1980", MONTH = "", NOTE = "", REVIEW = "" ) @ARTICLE(pebble:ic, AUTHOR = "Lampson, B. and Burstall, R.", TITLE = "Pebble, a Kernel Language for Modules and Abstract Data Types", JOURNAL = "Information and Computation", YEAR = "1988", VOLUME = "76", NUMBER = "2/3", PAGES = "", MONTH = "", NOTE = "", REVIEW = "" ) @ARTICLE(bohm:coding, AUTHOR = "B{\"{o}}hm, C. and Berarducci, A.", TITLE = "Automatic Synthesis of Typed $\lambda$-programs on Term Algebras", JOURNAL = "Theoretical Computer Science", YEAR = "1985", VOLUME = "39", NUMBER = "", PAGES = "", MONTH = "", NOTE = "", REVIEW = "impredicative coding of data types" ) @ARTICLE(pebble:84, AUTHOR = "Burstall, R. and Lampson, B.", TITLE = "Pebble, a Kernel Language for Modules and Abstract Data Types", JOURNAL = LNCS, YEAR = "1984", VOLUME = "173", NUMBER = "", PAGES = "", MONTH = "", NOTE = "", REVIEW = "" ) @BOOK(nuprl-book, AUTHOR = "Constable, R. and others", EDITOR = "", TITLE = "Implementing Mathematics with the NuPRL Proof Development System", PUBLISHER = "Pretice-Hall", YEAR = "1986", MONTH = "", EDITION = "", NOTE = "", REVIEW = "the Nuprl book") @BOOK(barendregt:lambda-book, AUTHOR = "Barendregt, H.P.", EDITOR = "", TITLE = "The Lambda Calculus: its Syntax and Semantics", PUBLISHER = "North-Holland", YEAR = "1984", MONTH = "", EDITION = "revised", REVIEW = "the lambda-calculus book" ) @BOOK(beeson:book, AUTHOR = "Beeson, M.J.", EDITOR = "", TITLE = "Foundations of Constructive Mathematics", PUBLISHER = "Springer-Verlag", YEAR = "1985", MONTH = "", EDITION = "", REVIEW = "", ) @BOOK(bishop:book, AUTHOR = "Bishop, E.", EDITOR = "", TITLE = "Foundations of Constructive Analysis", PUBLISHER = "McGraw-Hill", YEAR = "1967", MONTH = "", EDITION = "", REVIEW = "", ) @CONFERENCE(hope, AUTHOR = "Burstall, R. and MacQueen, D. and Sannella, D.", TITLE = "HOPE: an Experimental Applicative Language", BOOKTITLE = "1980 LISP Conference", YEAR = "1980", MONTH = "", EDITOR = "", PAGES = "", ORGANIZATION = "", PUBLISHER = "", ADDRESS = "California", NOTE = "", REVIEW = "" ) @InProceedings{burstall:pebblejapan, author = "Burstall, R.", title = "Programming with Modules as Typed Functional Programming", booktitle = "Proc. of Inter. Conf. on Fifth Generation Computer Systems", year = "1984", OPTeditor = "", OPTpages = "", OPTorganization = "", OPTpublisher = "", address = "Tokyo", OPTmonth = "", OPTnote = "" } @PHDTHESIS(luo:thesis, AUTHOR = "Luo, Z.", TITLE = "An Extended Calculus of Constructions", SCHOOL = "University of Edinburgh", YEAR = "1990", MONTH = "", ADDRESS = "", OPTNOTE = "Also as Report CST-65-90/ECS-LFCS-90-118, Department of Computer Science, University of Edinburgh", REVIEW = "" ) @PHDTHESIS(luo:thesisshort, AUTHOR = "Luo, Z.", TITLE = "An Extended Calculus of Constructions", SCHOOL = "University of Edinburgh", YEAR = 1990, MONTH = "", ADDRESS = "", NOTE = "", REVIEW = "" ) @MISC(berardi:jumelage89, AUTHOR = "Berardi, S", TITLE = "Non-conservativity of Coquand's Calculus with respect to Higher-order Intuitionistic Logic", HOWPUBLISHED = "Talk given in the 3rd Jumelage meeting on Typed Lambda Calculi, Edinburgh", YEAR = "1989", MONTH = "", NOTE = "", REVIEW = "" ) @MISC(bgeuvers:conservLF, AUTHOR = "Barendsen, E. and Geuvers, H.", TITLE = "Conservativity of $\lambda$P over PRED", HOWPUBLISHED = "manuscript", YEAR = "1989", MONTH = "", NOTE = "", REVIEW = "" ) @MISC(burstall:deliverable, AUTHOR = "Burstall, R.", TITLE = "An Approach to Program Specification and Development in Constructions", HOWPUBLISHED = "Talk given in Workshop on Programming Logic, Bastad, Sweden", YEAR = "1989", MONTH = "May", NOTE = "", REVIEW = "" ) @TechReport{burmck:deliverable-report, author = "Burstall, R. and McKinna, J.", title = "Deliverables: an approach to program development in the calculus of constructions", institution = "Dept of Computer Science, University of Edinburgh", year = "1991", type = "LFCS report", number = "ECS-LFCS-91-133", OPTaddress = "", OPTmonth = "", OPTnote = "" } @TechReport{burmck:deliverable-report92, author = "Burstall, R. and McKinna, J.", title = "Deliverables: a categorical approach to program development in type theory", institution = "Dept of Computer Science, University of Edinburgh", year = "1992", type = "LFCS report", number = "ECS-LFCS-92-242", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Misc{burmck:deliverable, author = "Burstall, R. and McKinna, J.", title = "Deliverables: an approach to program development in the calculus of constructions", howpublished = "In the preliminary Proceedings of the 1st Workshop on Logical Frameworks", year = "1990", OPTmonth = "", OPTnote = "" } @PhdThesis{mck:thesis, author = "McKinna, J.", title = "Deliverables: a categorical approach to program development in type theory", school = "Department of Computer Science, University of Edinburgh", year = "1992", OPTaddress = "", OPTmonth = "", OPTnote = "" } @TECHREPORT(asperti, AUTHOR = "Asperti, A.", TITLE = "The Internal Model of Polymorphic Lambda Calculus", TYPE = "Report", NUMBER = "CMU-CS-88-155", INSTITUTION = "Computer Science Dept., CMU", YEAR = "1988", MONTH = "", ADDRESS = "", NOTE = "", REVIEW = "" ) @UNPUBLISHED(barendregt:hb, AUTHOR = "Barendregt, H.P.", TITLE = "Typed Lambda Calculi", YEAR = "1989", MONTH = "", NOTE = "to appear in Handbook of Logic in Computer Science (eds., S. Abramsky, D. Gabbay and T.S.E. Maibaum) Oxford University Press", REVIEW = "" ) @UNPUBLISHED(barendregt:GTS, AUTHOR = "Barendregt, H.P.", TITLE = "Introduction to Generalized Type Systems", YEAR = "1989", MONTH = "", NOTE = "Proc. of the 3rd Italian Conf. on Theoretical Computer Science, Mandera.", REVIEW = "" ) @UNPUBLISHED(berardi:thesisman, AUTHOR = "Berardi, S.", TITLE = "Type Dependence and Constructive Mathematics", YEAR = "1989", MONTH = "June", NOTE = "manuscript", REVIEW = "thesis manuscript" ) @PhdThesis{berardi:thesis, author = "Berardi, S.", title = "Type Dependence and Constructive Mathematics", school = "Universita di Torino", year = "1990", address = "Italy", OPTmonth = "", OPTnote = "" } @Article{luo:ictheory, author = "Luo, Z.", title = "A Higher-order Calculus and Theory Abstraction", journal = "Information and Computation", year = "1991", volume = "90", number = "1", OPTpages = "107-137", OPTmonth = "", OPTnote = "" } @UNPUBLISHED(luo:ictheoryToAppear, AUTHOR = "Luo, Z.", TITLE = "A Higher-order Calculus and Theory Abstraction", YEAR = "1989", MONTH = "", NOTE = "To appear in Information and Computation", REVIEW = "" ) @UNPUBLISHED(burluo:strthynotes, AUTHOR = "Burstall, R. and Luo, Z.", TITLE = "A Set-theoretic Setting for Structuring Theories in Proof Development", YEAR = "1988", MONTH = "April", NOTE = "Circulated notes", REVIEW = "" ) @UNPUBLISHED(burluo:strthynotes90, AUTHOR = "Burstall, R. and Luo, Z.", TITLE = "A Set-theoretic Setting for Structuring Theories in Proof Development", YEAR = "1990", OPTMONTH= "April", NOTE = "manuscript", REVIEW = "" ) @TechReport{burluo:strthyReport, author = "Z. Luo and R. Burstall", title = "A Set-theoretic Setting for Structuring Theories in Proof Development", institution = "Department of Computer Science, University of Edinburgh", year = "1992", type = "LFCS Report Series", number = "ECS-LFCS-92-206", OPTaddress = "", OPTmonth = "", OPTnote = "" } @InProceedings{burstall:proofeng, author = "Burstall, R.", title = "Research in Interactive Theorem Proving at Edinburgh University", booktitle = "Proc. of 20th IBM Computer Science Symposium", year = "1986", OPTeditor = "", OPTpages = "", OPTorganization = "", OPTpublisher = "", address = "Shizuoka, Japan", OPTmonth = "", note = "Also, LFCS Report ECS-LFCS-86-12, Dept. of Computer Science, Univ. of Edinburgh" } @Unpublished{burstall:introLego, author = "Burstall, R.", title = "Computer-assisted Proof for Mathematics: an introduction, using the LEGO proof system", note = "To appear in Proc. of the Institute for Applied Math. conf., Brighton Polytechnic", year = "1989", OPTmonth = "" } @Article{cardelli:subtype, author = "Cardelli, L.", title = "Type-checking Dependent Types and Subtypes", journal = LNCS, year = "1988", volume = "306", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Unpublished{cardelli:typetype, author = "Cardelli, L.", title = "A Polymorphic $\lambda$-calculus with Type:Type", note = "manuscript", year = "1986", OPTmonth = "" } @Unpublished{cardelli:typeful, author = "Cardelli, L.", title = "Typeful Programming", note = "Lecture notes for the IFIP State of the Art Seminar on Formal Description of Programming Concepts, Rio de Janeiro, Brazil", year = "1989", OPTmonth = "" } @PhdThesis{cartmell:thesis, author = "Cartmell, J.", title = "Generalized Algebraic Theories and Contextual Category", school = "University of Oxford", year = "1978", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{cartmell:ctxtjournal, author = "Cartmell, J.", title = "Generalized Algebraic Theories and Contextual Category", journal = "Annals of Pure and Applied Logic", year = "1986", volume = "32", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Book{curryfeys:book, author = "Curry, H.B. and Feys, R.", title = "Combinatory Logic", publisher = "North Holland Publishing Company", year = "1958", OPTeditor = "", volume = "1", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", REVIEW = "props-as-types principle" } @TechReport{coqetc:polymodel, author = "Coquand, Th. and Gunter, C. and Winskel, G.", title = "Domain Theoretic Models of Polymorphism", institution = "Computer Laboratory, University of Cambridge", year = "1987", type = "Tech. Report", number = "116", OPTaddress = "", OPTmonth = "", OPTnote = "", REVIEW = "domain-theoretic model for F, also appear in a journal?" } @Article{CoqHue:CC85, author = "Coquand, Th. and Huet, G.", title = "Constructions: a Higher Order Proof System for Mechanizing Mathematics", journal = "Lecture Notes in Computer Science", year = "1985", volume = "203", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", REVIEW = "Constructions, with examples and implementation description" } @Article{CoqHue:icCC, author = "Coquand, Th. and Huet, G.", title = "The Calculus of Constructions", journal = "Information and Computation", year = "1988", volume = "76", number = "2/3", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{HarPol:univpoly89, author = "Harper, R. and Pollack, R.", title = "Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions", journal = "Theoretical Computer Science", year = "1989", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "to appear" } @Article{HarPol:univpoly-TCS, author = "Harper, R. and Pollack, R.", title = "Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions", journal = "Theoretical Computer Science", year = "1991", volume = "89", number = "1", OPTpages = "", OPTmonth = "", OPTnote = "" } @Unpublished{huet:univpoly87, author = "Huet, G.", title = "A Calculus with Type:Type", note = "unpublished manuscript", year = "1987", OPTmonth = "" } @Article{church:hol40, author = "Church, A.", title = "A Formulation of the Simple Theory of Types", journal = "J. Symbolic Logic", year = "1940", volume = "5", number = "1", OPTpages = "", OPTmonth = "", OPTnote = "" } @InProceedings{constable:71, author = "Constable, R.L.", title = "Constructive Mathematics and Automatic Programs Writers", booktitle = "Proc. IFIP'71", year = "1971", OPTeditor = "", OPTpages = "", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "" } @PhdThesis{coq:thesis, author = "Coquand, Th.", title = "Une Theorie des Constructions", school = "University of Paris VII", year = "1985", OPTaddress = "", OPTmonth = "", OPTnote = "" } @InProceedings{coq:paradox, author = "Coquand, Th.", title = "An Analysis of {Girard}'s Paradox", booktitle = "Proc. 1st Ann. Symp. on Logic in Computer Science", year = "1986", OPTeditor = "", OPTpages = "", organization = "IEEE", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "", REVIEW = "GCC, paradox for $\Sigma$ and two-level impredicativity" } @Unpublished{coq:proofSN, author = "Coquand, Th.", title = "A Calculus of Constructions", note = "manuscript", year = "1986", OPTmonth = "" } @Unpublished{coq:metaCC, author = "Coquand, Th.", title = "Metamathematical Investigations of a Calculus of Constructions", note = "manuscript", year = "1989", OPTmonth = "", REVIEW = "also in some collection book?" } @Article{CoqMoh:indtypes90, author = "Coquand, Th. and Paulin-Mohring, Ch.", title = "Inductively Defined Types", journal = LNCS, year = "1990", volume = "417", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", REVIEW = "using ECC to discuss ind types" } @Article{CarWeg:survey, author = "Cardelli, L. and Wegner, P.", title = "On Understanding Types, Data Abstraction and Polymorphism", journal = "Computing Surveys", year = "1985", volume = "17", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Misc{deBruijn:index, author = "de Bruijn, N.G.", title = "Lambda Calculus Notation with Nameless Dummies: a Tool for Automatic Formula Manipulation with Application to the Church-Rosser Theorem", howpublished = "Indag. Mathematics 34", year = "1972", OPTmonth = "", OPTnote = "" } @InCollection{deBruijn:Automath80, author = "de Bruijn, N.G.", title = "A Survey of the Project {AUTOMATH}", booktitle = "To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism", publisher = "Academic Press", year = "1980", editor = "Hindley, J. and Seldin, J.", OPTchapter = "", OPTpages = "", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{guttagetc:ADT, author = "Guttag, J.V. and Horowitz, E. and Musser, D.R.", title = "Abstract Data Types and Software Validation", journal = "Comm. ACM", year = "1976", volume = "21", number = "12", OPTpages = "", OPTmonth = "", OPTnote = "", REVIEW = "equality representation or representation invariants" } @Unpublished{pollack:implicit90, author = "Pollack, R.", title = "Implicit Syntax", note = "In the preliminary Proceedings of the 1st Workshop on Logical Frameworks", year = "1990", OPTmonth = "" } @Unpublished{pollack:legothy, author = "Pollack, R.", title = "The Theory of {LEGO}", note = "manuscript", year = "1989", OPTmonth = "" } @Unpublished{pollack:tarski, author = "Pollack, R.", title = "The {Tarski} Fixpoint Theorem", note = "communication on TYPES e-mail network", year = "1990", OPTmonth = "" } @Manual{legomanual, title = "How to Use LEGO: a preliminary user's manual", author = "Luo, Z. and Pollack, R. and Taylor, P.", organization = "LFCS Technical Notes LFCS-TN-27, Dept. of Computer Science, Edinburgh University", OPTaddress = "", OPTedition = "", year = "1989", OPTmonth = "", OPTnote = "" } @Book{NPS:book, author = "Nordstr{\"{o}}m, B. and Petersson, K. and Smith, J.", title = "Programming in {\ML}'s Type Theory", publisher = "Oxford University Press", year = "1990", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Unpublished{NPS:chapter94, author = "Nordstr{\"{o}}m, B. and Petersson, K. and Smith, J.", title = "{\ML}'s Type Theory", note = "Manuscript", OPTcrossref = "", OPTkey = "", year = "1994", OPTmonth = "", OPTannote = "" } @Unpublished{ML:71, author = "Martin-L{\"{o}}f, P.", title = "An Intuitionistic Theory of Types", note = "manuscript", year = "1971", OPTmonth = "" } @Unpublished{ML:72, author = "Martin-L{\"{o}}f, P.", title = "An Intuitionistic Theory of Types", note = "manuscript", year = "1972", OPTmonth = "" } @InProceedings{ML:73, author = "Martin-L{\"{o}}f, P.", title = "An Intuitionistic Theory of Types: predicative part", booktitle = "Logic Colloquium'73", year = "1975", editor = "H.Rose and J.C.Shepherdson", OPTpages = "", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "" } @InProceedings{ML:ConMathandProg82, author = "Martin-L{\"{o}}f, P.", title = "Constructive Mathematics and Computer Programming", booktitle = "Logic, Methodology and Philosophy of Science VI", year = "1982", editor = "{L.J. Cohen \etal}", OPTpages = "", OPTorganization = "", publisher = "North-Holland", address = "Amsterdam", OPTmonth = "", OPTnote = "" } @Book{ML:book84, author = "P. Martin-L{\"{o}f}", title = "Intuitionistic Type Theory", publisher = "Bibliopolis", year = "1984", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Unpublished{ML:meaning85, author = "Martin-L{\"{o}f}, P.", title = "Truth of a proposition, evidence of a judgement, validity of a proof", note = "Talk given at Workshop of Theories of Meaning, Florence", year = "1985", month = "June" } @InProceedings{luo:lics89, author = "Luo, Z.", title = "{\bf {ECC}}, an Extended Calculus of Constructions", booktitle = "Proc. of IEEE Fourth Ann. Symp. on Logic in Computer Science", year = "1989", OPTeditor = "", OPTpages = "", OPTorganization = "IEEE", OPTpublisher = "", address = "Asilomar, California, U.S.A.", month = "June", OPTnote = "" } @InProceedings{luo:lics89short, author = "Luo, Z.", title = "{\bf {ECC}}, an Extended Calculus of Constructions", booktitle = "Proc. of LICS'89", year = "1989", OPTeditor = "", OPTpages = "", OPTorganization = "IEEE", OPTpublisher = "", OPTaddress = "Asilomar, California, U.S.A.", OPTmonth = "June", OPTnote = "" } @TechReport{luo:adequacy, author = "Luo, Z.", title = "A Problem of Adequacy: conservativity of calculus of constructions over higher-order logic", institution = "LFCS report series ECS-LFCS-90-121, Department of Computer Science, University of Edinburgh", year = "1990", OPTtype = "", OPTnumber = "", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Unpublished{tayluo:theorynotes, author = "Taylor, P. and Luo, Z.", title = "Theories, Mathematical Structures and Strong Sums", note = "manuscript", year = "1988", month = "December" } @Article{santar:specinst88, author = "Sannella, D. and Tarlecki, A.", title = "Specifications in Arbitrary Institutions", journal = "Information and Computation", year = "1988", volume = "76", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{santar:impl, author = "Sannella, D. and Tarlecki, A.", title = "Toward Formal Development of Programs from Algebraic Specifications: implementation revisited", journal = "Acta Informatica", year = "1988", volume = "25", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", REVIEW = "Also LFCS Report Series ECS-LFCS-86-17" } @TechReport{santar:para90, author = "Sannella, D. and Sokolowski, S. and Tarlecki, A.", title = "Toward Formal Development of Programs from Algebraic Specifications: Parameterization Revisited", institution = "Dept. of Computer Science, University of Edinburgh", year = "1992", type = "LFCS Report Series", number = "ECS-LFCS-92-222", OPTaddress = "", OPTmonth = "", OPTnote = "" } @TechReport{santar:para-report92, author = "Sannella, D. and Sokolowski, S. and Tarlecki, A.", title = "Toward Formal Development of Programs from Algebraic Specifications: Parameterization Revisited", institution = "Department of Computer Science, University of Edinburgh", year = "1992", type = "LFCS Report", number = "ECS-LFCS-92-222", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Unpublished{ore:ind90, author = "Ore, C.-E.", title = "The {Extended Calculus of Constructions} ({{\bf ECC}}) with inductive types", note = "To appear in Information and Computation", year = "1990", OPTmonth = "" } @Article{ore:indIC92, author = "Ore, C.-E.", title = "The {Extended Calculus of Constructions} ({{\bf ECC}}) with inductive types", journal = "Information and Computation", year = "1992", volume = "99", number = "2", pages = "231-264", OPTmonth = "", OPTnote = "" } @Article{beeson:extoprn, author = "Beeson, M.J.", title = "Problematic Principles in Constructive Mathematics", journal = "Logic Colloquium'80", year = "1982", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Book{Ehrig:book85, author = "Ehrig, H. and Mahr, B.", title = "Fundamentals of Algebraic Specification 1: Equations and Initial Semantics", publisher = "Springer", year = "1985", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Book{Ehrig:book90, author = "Ehrig, H. and Mahr, B.", title = "Fundamentals of Algebraic Specification 2: Module specifications and Constraints", publisher = "Springer", year = "1990", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Misc{Maibaumetc:impl83, author = "Maibaum, T.S.E. and Sadler, M.R. and Veloso, P.A.S.", title = "Logical Implementation", OPThowpublished = "", year = "1983", OPTmonth = "", OPTnote = "" } @Article{OBJ2, author = "K. Futatsugi and J. Goguen and J.-P. Jouannaud and J. Meseguer", title = "Principles of {OBJ2}", journal = "Proc. Principles of Programming Languages. {ACM}", year = "1985", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @TechReport{Act1, author = "H. Ehrig and W. Fey and H. Hansen", title = "{ACT} {ONE}: an Algebraic Specification Language with Two Levels of Semantics", institution = "Technical University of Berlin, Fachbereich Informatik", year = "1983", OPTtype = "", number = "83-03", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{WirBroy:ultra89, author = "Wirsing, M. and Broy, M.", title = "A Modular Framework for Specification and Implementation", journal = "TAPSOFT'89, LNCS", year = "1989", volume = "351", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{Mohring:popl89, author = "Ch. Paulin-Mohring", title = "Extracting {$F^\w$} Programs from Proofs in the Calculus of Constructions", journal = "Proc. Principles of Programming Languages", year = "1989", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{backhouse:doit89, author = "R. Backhouse and P. Chisholm and G. Malcolm", title = "Do-it-Youself Type Theory", journal = "Formal Aspects of Computing", year = "1989", volume = "1", number = "1", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{hoare:refn72, author = "C.A.R. Hoare", title = "Proofs of correctness of data representation", journal = "Acta Informatica", year = "1972", volume = "1", number = "1", OPTpages = "", OPTmonth = "", OPTnote = "" } @InCollection{Gogetc:ADT78, author = "J.A. Goguen and J.W. Thatcher and E.G. Wagner", title = "Abstract Data Types as Initial Algebras and the Correctness of Data Representation", booktitle = "Current Trends in Programming Methodology, Vol. 4", publisher = "Prentice Hall", year = "1978", editor = "R. Yeh", OPTchapter = "", OPTpages = "", OPTaddress = "", OPTmonth = "", OPTnote = "" } @TechReport{SanWir:ASL83, author = "D.T. Sannella and M. Wirsing", title = "A Kernal Language for Algebraic Specification and Implementation", institution = "Dept of Computer Science, University of Edinburgh", year = "1983", OPTtype = "", number = "CSR-155-83", OPTaddress = "", OPTmonth = "", OPTnote = "" } @TechReport{gogbur:CAT80, author = " Goguen, J. and Burstall, R.", title = "CAT: a System for the structured elaboration of correct programs and from structured specifications", institution = "SRI International", year = "1980", type = "Tech Report", number = "CSL-118", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Book{HinSel:book87, author = "J.R. Hindley and J.P. Seldin", title = "Introduction to Combinators and $\lambda$-calculus", publisher = "Cambridge University Press", year = "1987", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @TechReport{Luo:UTTreport, author = "Luo, Z.", title = "A Unifying Theory of Dependent Types {I}", institution = "LFCS report series ECS-LFCS-91-154", year = "1991", OPTtype = "", OPTnumber = "", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Unpublished{Luo:UTTnotes90-11-21, author = "Luo, Z.", title = "A Unifying Theory of Dependent Types {I}", note = "manuscript", year = "1990", month = "November" } @Unpublished{Luo:UTTnotes90-12-13, author = "Luo, Z.", title = "A Unifying Theory of Dependent Types {I}", note = "manuscript", year = "1990", month = "December" } @Unpublished{Luo:UTT91-04-18, author = "Luo, Z.", title = "A Unifying Theory of Dependent Types {I}", note = "manuscript", year = "1991", month = "April" } @Unpublished{Salvesen:eta89, author = "Salvesen, A.", title = "The Church-Rosser Theorem for LF with $\beta\eta$ reduction", note = "manuscript", year = "1989", OPTmonth = "" } @Book{LamSco:book86, author = "J. Lambek and P.J. Scott", title = "Introduction to Higher-Order Categorical Logic", publisher = "Cambridge University Press", year = "1986", OPTeditor = "", volume = "VII", series = "Cambridge Studies in Advanced Mathematics", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Misc{Jay:SNnote90, author = "Jay, B.", OPTtitle = "", howpublished = "personal communication", year = "1990", OPTmonth = "", OPTnote = "" } @Article{Wirsing:ASL86, author = "M. Wirsing", title = "Structured Algebraic Specifications: a kernel language", journal = "Theoretical Computer Science", year = "1986", volume = "42", OPTnumber = "", pages = "123-249", OPTmonth = "", OPTnote = "" } @Article{Ehrigetc:impl82, author = "H. Ehrig and H. Kreowski and B. Mahr and P. Padawitz", title = "Algebraic implementation of abstract data types", journal = "Theoretical Computer Science", year = "1982", volume = "20", OPTnumber = "", pages = "209-263", OPTmonth = "", OPTnote = "" } @Article{LisZil:ADT75, author = "B. Liskov and S. Zilles", title = "Specification techniques for data abstraction", journal = "IEEE Trans. on Software Engineering", year = "1975", volume = "SE-1", number = "1", OPTpages = "", OPTmonth = "", OPTnote = "" } @Book{Jones:book86, author = "C.B. Jones", title = "Systematic Software Development using VDM", publisher = "Prentice-Hall", year = "1986", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Article{santar:EML87, author = "D. Sannella and A. Tarlecki", title = "Extended {ML}: an institution-independent framework for formal program development", journal = "Proc. Workshop on Category Theory and Computer Programming, {LNCS 240}", year = "1987", OPTvolume = "", OPTnumber = "", pages = "364-389", OPTmonth = "", OPTnote = "" } @Article{NorPet:spec83, author = "Nordstr{\"{o}}m, B. and Petersson, K.", title = "Types and Specifications", journal = "Proceedings of IFIP'83", year = "1983", OPTvolume = "", OPTnumber = "", pages = "915-920", OPTmonth = "", OPTnote = "" } @Article{MacQ:SMLmodule81, author = "D.D. MacQueen", title = "Structures and parameterization in a typed functional language", journal = "Proc. Symp. on Functional Programming and Computer Architecture", year = "1981", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Book{Milner:bookSMLdefn, author = "R. Milner and M. Tofte and R. Harper", title = "The Definition of Standard ML", publisher = "MIT", year = "1990", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Article{Gir:71, author = "J.-Y. Girard", title = "Une extension de l'interpretation fonctionelle de G{\"{o}}del \`{a} l'analyse et son application {\`{a}} l'{\'{e}}limination des coupures dans et la th\`{e}orie des types'", journal = "Proc. 2nd Scandinavian Logic Symposium. {\rm \mbox{North-Holland}}", year = "1971", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @PhdThesis{Girard:thesis, author = "J.-Y. Girard", title = "Interpr\'{e}tation fonctionelle et \'{e}limination des coupures de l'arithm\'{e}tique d'ordre sup\'{e}rieur", school = "Universit\'{e} Paris VII", year = "1972", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{Gir:73, author = "J.-Y. Girard", title = "Quelques r\'{e}sultats sur les interpr\'{e}tations fonctionells", journal = "Lecture Notes in Mathematics 337. {\rm Springer}", year = "1973", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{Reynolds:poly74, author = "J.C. Reynolds", title = "Towards a Theory of Type Structure", journal = "Lecture Notes in Computer Science", year = "1974", volume = "19", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Unpublished{luo:indnotes90, author = "Z. Luo", title = "A Unifying Theory of Dependent Types", note = "manuscript.", year = "1990", OPTmonth = "" } @Unpublished{santar:holtype90, author = "Sannella, D. and Tarlecki, A.", title = "A Kernel Specification Formalism with Higher-order Parameterization", note = "Draft", year = "1990", OPTmonth = "" } @Article{Ehr:modelCC, author = "T. Ehrhard", title = "A Categorical Semantics of Constructions", journal = "Proc. 3rd Ann. Symp. on Logic in Computer Science, Edinburgh. {IEEE}", year = "1988", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{Friedman:77, author = "H. Friedman", title = "Set-theoretic Foundations for Constructive Analysis", journal = "Annals of Mathematics", year = "1977", volume = "105", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @InProceedings{Galier:cand89, author = "J.H. Gallier", title = "On {Girard's} `{Candidats de Reductibilit\'{e}}'", booktitle = "Logic and Computer Science", year = "1990", editor = "P. Odifreddi", OPTpages = "", OPTorganization = "", publisher = "Academic Press", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{Girard:15yrs86, author = "J.-Y. Girard", title = "The System {F} of Variable Types, Fifteen Years Later", journal = "Theoretical Computer Science", year = "1986", volume = "45", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Book{Giretc:prftypes90, author = "J.-Y. Girard and Y. Lafont and P. Taylor", title = "Proofs and Types", publisher = "Cambridge University Press", year = "1990", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @InProceedings{Hayashi:review89, author = "S. Hayashi", title = "Constructive Mathematics and Computer-assisted Reasoning Systems", booktitle = "Proc. of Heyting'88", year = "1989", OPTeditor = "", OPTpages = "", OPTorganization = "", OPTpublisher = "Prenum Press", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{Hayashi:ATT, author = "S. Hayashi", title = "Singleton, Union and Intersection Types in Program Extraction", journal = "Lecture Notes in Computer Science", year = "1991", volume = "526", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "Revised version to appear in Information and Computation." } @Article{Hayashi:ATT94, author = "S. Hayashi", title = "Singleton, Union and Intersection Types for Program Extraction", journal = "Information and Computation", year = "1994", volume = "109", number = "1/2", pages = "174-210", OPTmonth = "", OPTnote = "" } @Book{Heyting:71, author = "A. Heyting", title = "Intuitionism: An Introduction", publisher = "North-Holland", year = "1971", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Article{LF:87, author = "R. Harper and F. Honsell and G. Plotkin", title = "A Framework for Defining Logics", journal = "Proc. 2nd Ann. Symp. on Logic in Computer Science. {IEEE}", year = "1987", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @InProceedings{How:69, author = "W. A. Howard", title = "The Formulae-as-types Notion of Construction", booktitle = "{To H. B. Curry: Essays on Combinatory Logic}", year = "1980", editor = "J. Hindley and J. Seldin", OPTpages = "", OPTorganization = "", publisher = "Academic Press", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{HylPit:modelCC87, author = "M. Hyland and A. Pitts", title = "The Theory of Constructions: categorical semantics and topos-theoretic models", journal = "Categories in Computer Science and Logic, Boulder", year = "1987", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{Huet:sets87, author = "G. Huet", title = "Induction Principles Formalized in the Calculus of Constructions", journal = "{TAPSOFT'87}, {LNCS'249}", year = "1987", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{MitPlo:abstype85, author = "J. Mitchell and G. Plotkin", title = "Abstract Types Have Existential Type", journal = "Proc. 12th Principles of Programming Languages", year = "1985", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{Myhill:75, author = "J. Myhill", title = "Constructive Set Theory", journal = "J. Symbolic Logic", year = "1975", volume = "40", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Book{CamLCF:book87, author = "L. Paulson", title = "Logic and Computation: Interactive Proof with Cambridge LCF", publisher = "Cambridge University Press", year = "1987", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @TechReport{Pottinger:metaCC87, author = "G. Pottinger", title = "Strong Normalization for Terms of the Theory of Constructions", institution = "Odyssey Research Associates", year = "1987", OPTtype = "", number = "TR 11-7", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{Reynolds:83, author = "J. C. Reynolds", title = "Types, Abstraction and Parameter Polymorphism", journal = "Information Processing'83", year = "1983", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{Reynolds:setmodel84, author = "J. C. Reynolds", title = "Polymorphism is Not Set-theoretic", journal = "Lecture Notes in Computer Science", year = "1984", volume = "173", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @TechReport{ReyPlo:setmodel88, author = "J. C. Reynolds and G. D. Plotkin", title = "On Functors Expressible in the Polymorphic Typed Lambda Calculus", institution = "Dept. of Computer Science, Univ. of Edinburgh", year = "1988", type = "LFCS report", number = "ECS-LFCS-88-53", OPTaddress = "", OPTmonth = "", OPTnote = "" } @PhdThesis{Streicher:thesis, author = "T. Streicher", title = "Correctness and Completeness of a Categorical Semantics of the Calculus of Constructions", school = "Passau", year = "1988", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{Tait:67, author = "W.W. Tait", title = "Intensional Interpretation of Functionals of Finite Type I", journal = "J. of Symbolic Logic", year = "1967", volume = "32", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @InProceedings{Tait:75, author = "W. W. Tait", title = "A Realizability Interpretation of the Theory of Species", booktitle = "Logic Colloquium, Lecture Notes in Mathematics, 453", year = "1975", editor = "R. Parikh", OPTpages = "", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "" } @PhdThesis{vanDaalen:thesis, author = "D. T. van Daalen", title = "The Language Theory of Automath", school = "Technological University", year = "1980", address = "Eindhoven", OPTmonth = "", OPTnote = "" } @Book{TrovanDalen:book, author = "A.S. Troelstra and D. van Dalen", title = "Constructivism in Mathematics, an introduction", publisher = "North-Holland", year = "1988", OPTeditor = "", volume = "I and II", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Book{Andrews:book, author = "P.B. Andrews", title = "An Introduction to Mathematical Logic and Type Theory: to truth through proof", publisher = "Academic Press", year = "1986", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @InProceedings{Dummett:73, author = "M. Dummett", title = "The philosophical foundations of intuitionistic logic", booktitle = "Logic Colloquium'73", year = "1975", editor = "H.Rose and J.C.Shepherdson", pages = "5-40", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{Smith:peano4, author = "J. Smith", title = "The independence of {Peano}'s fourth axiom from {\ML}'s type theory without universes", journal = "Journal of Symbolic Logic", year = "1988", volume = "53", number = "3", OPTpages = "", OPTmonth = "", OPTnote = "" } @TechReport{LongoMoggi:wset88, author = "G. Longo and E. Moggi", title = "Constructive Natural Deduction and Its `Modest' Interpretation", institution = "Computer Science Dept., Carnegie Mellon Univ.", year = "1988", type = "Report", number = "CMU-CS-88-131", OPTaddress = "", OPTmonth = "", OPTnote = "" } @InProceedings{Hyland:Eff82, author = "M. Hyland", title = "The Effective Topos", booktitle = "The Brouwer Symposium", year = "1982", editor = "A.S. Troelstra and {van Dalen}", OPTpages = "", OPTorganization = "", publisher = "North-Holland", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{Hyland:87, author = "M. Hyland", title = "A Small Complete Category", journal = "Annals of Pure and Applied Logic", year = "1988", volume = "40", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{Luo:tapsoft91, author = "Z. Luo", title = "Program specification and data refinement in type theory", journal = "Proc. of the Fourth Inter. Joint Conf. on the Theory and Practice of Software Development (TAPSOFT), LNCS 493", year = "1991", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "Also as LFCS report ECS-LFCS-91-131, Dept. of Computer Science, Edinburgh University" } @TechReport{INRIA:CC, author = "G. Huet", title = "(ed.) The Calculus of Constructions: Documentation and User's Guide", institution = "INRIA", year = "1989", type = "Technical Report", number = "INRIA 110", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{GogBur:inst84, author = "J. Goguen and R. Burstall", title = "Introducing Institutions", journal = "{LNCS} 164", year = "1984", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @TechReport{GogBur:inst90, author = "J. Goguen and R. Burstall", title = "Institutions: abstract model theory for specification and programming", institution = "LFCS, Dept of Computer Science, University of Edinburgh", year = "1990", OPTtype = "", number = "ECS-LFCS-90-106", OPTaddress = "", OPTmonth = "", OPTnote = "" } @InProceedings{Mes:GL89, author = "J. Meseguer", title = "General Logics", booktitle = "Logic Colloquium 1987", year = "1989", editor = "{H.-D. Ebbinghaus} et al", OPTpages = "", OPTorganization = "", publisher = "{North-Holland}", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{ST:obs87, author = "Sannella, D. and Tarlecki, A.", title = "On observational equivalence and algebraic specification", journal = "Computer and System Science", year = "1987", volume = "34", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @InProceedings{coquand:eta91, author = "Th. Coquand", title = "An algorithm for testing conversion in {Type Theory}", booktitle = "Logical Frameworks", year = "1991", editor = "G. Huet and G. Plotkin", OPTpages = "", OPTorganization = "", publisher = "Cambridge University Press", OPTaddress = "", OPTmonth = "", OPTnote = "" } @InProceedings{Dybjer:ind-types88, author = "P. Dybjer", title = "Inductively defined sets in {\ML}'s set theory", booktitle = "Workshop on General Logic", year = "1988", editor = "A. Avron et al", OPTpages = "", OPTorganization = "", publisher = "LFCS Report Series, ECS-LFCS-88-52, Dept. of Computer Science, University of Edinburgh", OPTaddress = "", OPTmonth = "", OPTnote = "" } @InProceedings{Dybjer:inv89, author = "P. Dybjer", title = "An Inversion Principle for {\ML}'s Type Theory", booktitle = "Workshop on Programming Logic", year = "1989", editor = "P. Dybjer et al", OPTpages = "", OPTorganization = "", publisher = "Programming Methodology Group, Report 54", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{Dybjer:bastad, author = "Peter Dybjer", title = "Inductive Families", journal = "Formal Aspects of Computing", year = "1993", note = "To appear." } @InProceedings{Dybjer:ind-types91, author = "P. Dybjer", title = "Inductive sets and families in {\ML}'s type theory and their set-theoretic semantics", booktitle = "Logical Frameworks", year = "1991", editor = "G. Huet and G. Plotkin", OPTpages = "", OPTorganization = "", publisher = "Cambridge University Press", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{Dybjer:94, author = "P. Dybjer", title = "A general formulation of simultaneous inductive-recursive definitions in type theory", OPTcrossref = "", OPTkey = "", OPTjournal = "", year = "1994", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @InProceedings{Aczel:inter3, author = "P. Aczel", title = "The type theoretic interpretation of constructive set theory: inductive definitions", booktitle = "Logic, Methodology and Philosophy of Science VII", year = "1986", OPTeditor = "", OPTpages = "", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Unpublished{aczel:classes, author = "P. Aczel", title = "Simple overloading for type theories", note = "Manuscript", OPTcrossref = "", OPTkey = "", year = "1994", OPTmonth = "", OPTannote = "" } @Misc{streicher:eqnotes91, author = "T. Streicher", OPTtitle = "", howpublished = "private communication", year = "1991", OPTmonth = "", OPTnote = "" } @InProceedings{Backhouse:datatype88, author = "R. Backhouse", title = "On the Meaning and Construction of the Rules in {\ML}'s Theory of Types", booktitle = "Workshop on General Logic", year = "1988", editor = "A. Avron \etal", OPTpages = "", OPTorganization = "", publisher = "LFCS Report Series, ECS-LFCS-88-52, Dept. of Computer Science, University of Edinburgh", OPTaddress = "", OPTmonth = "", OPTnote = "" } @PhdThesis{Mendler:thesis, author = "N. Mendler", title = "Recursive Definition in Type Theory", school = "Cornell University", year = "1988", OPTaddress = "", OPTmonth = "", OPTnote = "" } @InProceedings{Mendler:rec87, author = "N. Mendler", title = "Recursive Types and Type Constraints in Second-Order Lambda Calculus", booktitle = "Proceedings of POPL", year = "1987", OPTeditor = "", OPTpages = "", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "" } @InProceedings{Coq:ALF, author = "L. Augustsson and Th. Coquand and B. Nordstr{\"{o}}m", title = "A Short Description of Another Logical Framework", booktitle = "Preliminary Proc. of Logical Frameworks", year = "1990", editor = "G. Huet and G. Plotkin", OPTpages = "", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{ALF:92, author = "L. Magnusson", title = "The new implementation of {ALF}", OPTcrossref = "", OPTkey = "", journal = "Informal Proceedings of Workshop on Logical Frameworks, Bastad", year = "1992", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{ALF:94, author = "L. Magnusson and B. Nordstr{\"{o}}m", title = "The {ALF} proof editor and its proof engine", OPTcrossref = "", OPTkey = "", journal = "{LNCS} 806", year = "1994", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @InProceedings{curien:eta91, author = "P.-L. Curien and R. Di Cosmo", title = "A confluent reduction for the $\lam$-calculus with surjective pairing and terminal object", booktitle = "Proc. {ICALP}'91", year = "1991", OPTeditor = "", OPTpages = "", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Unpublished{GogLuo:W91, author = "H. Goguen and Z. Luo", title = "Inductive Data types: Well-Ordering Types Revisited", note = "submitted manuscript", year = "1991", OPTmonth = "" } @InProceedings{GogLuo:W92, author = "H. Goguen and Z. Luo", title = "Inductive Data types: Well-Ordering Types Revisited", booktitle = "Logical Frameworks", year = "1992", editor = "G. Huet and G. Plotkin", OPTpages = "", OPTorganization = "", publisher = "Cambridge University Press", OPTaddress = "", OPTmonth = "", note = "(To appear.) Also as LFCS Report Series ECS-LFCS-92-209, Dept of Computer Science, University of Edinburgh" } @InProceedings{GogLuo:LE93, author = "H. Goguen and Z. Luo", title = "Inductive Data types: Well-Ordering Types Revisited", booktitle = "Logical Environments", year = "1993", editor = "G. Huet and G. Plotkin", OPTpages = "", OPTorganization = "", publisher = "Cambridge University Press", OPTaddress = "", OPTmonth = "", note = "Also as LFCS Report Series ECS-LFCS-92-209, Dept of Computer Science, University of Edinburgh" } @InProceedings{GogLuo:LE93-only, author = "H. Goguen and Z. Luo", title = "Inductive Data types: Well-Ordering Types Revisited", booktitle = "Logical Environments", year = "1993", editor = "G. Huet and G. Plotkin", OPTpages = "", OPTorganization = "", publisher = "Cambridge University Press", OPTaddress = "", OPTmonth = "", OPTnote = "Also as LFCS Report Series ECS-LFCS-92-209, Dept of Computer Science, University of Edinburgh" } @InProceedings{claire:LE93, author = "C. Jones", title = "Completing the Rationals and Metric Spaces in {LEGO}", booktitle = "Logical Environments", year = "1993", editor = "G. Huet and G. Plotkin", OPTpages = "", OPTorganization = "", publisher = "Cambridge University Press", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Manual{Coq-manual, title = "The Coq Proof Assistent: User's Guide (version 5.6)", author = "G. Dowek and others", organization = "{INRIA}-Rocquencourt and {CNRS-ENS} Lyon", OPTaddress = "", OPTedition = "", year = "1991", OPTmonth = "", OPTnote = "" } @Manual{Coq-manual-v6.1, title = "The Coq Proof Assistant Reference Manual (version 6.1)", author = "Coq", organization = "{INRIA}-Rocquencourt and {CNRS-ENS} Lyon", year = "1996", } @Manual{Coq-manual-v6.3.1, title = {The Coq Proof Assistant Reference Manual (Version 6.3.1)}, OPTkey = {}, author = {B. Barras and others}, organization = {{INRIA}-Rocquencourt}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, year = {2000}, OPTnote = {}, OPTannote = {} } @InProceedings{Dummett:IL75, author = "M. Dummett", title = "The philosophical basis of intuitionistic logic", booktitle = "Proc. of the Logic Colloquium, 1973", year = "1975", editor = "H. Rose and J. Shepherdson", OPTpages = "", OPTorganization = "", publisher = "North Holland", OPTaddress = "", OPTmonth = "", note = "Reprinted in P. Benacerraf and H. Putnam (eds.), Philosophy of Mathematics: selected readings, Cambridge University Press." } @Book{Dummett:book91, author = "M. Dummett", title = "The Logical Basis of Metaphysics", publisher = "Duckworth", year = "1991", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Article{Prawitz:74, author = "D. Prawitz", title = "On the idea of a general proof theory", journal = "Synthese", year = "1974", volume = "27", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @InProceedings{Prawitz:73, author = "D. Prawitz", title = "Towards a foundation of a general proof theory", booktitle = "Logic, Methodology, and Phylosophy of Science {IV}", year = "1973", editor = "{P. Suppes \etal}", OPTpages = "", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{Scott:70, author = "D. Scott", title = "Constructive Validity", journal = "Symp. on Automatic Demonstration, Lecture Notes in Mathematics 125", year = "1970", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Misc{luo:course-notes91, author = "Luo, Z.", title = "Type Theory, Logic and Computer Science", howpublished = "PG course notes", year = "1991", month = "January", OPTnote = "" } @Book{Thompson:book, author = "S. Thompson", title = "Type Theory and Functional Programming", publisher = "Addison-Wesley", year = "1991", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @TechReport{legomanual:Report, author = "Z. Luo and R. Pollack", title = "{LEGO} {Proof} {Development} {System}: {User's} {Manual}", institution = "Dept of Computer Science, Univ of Edinburgh", year = "1992", type = "LFCS Report", number = "ECS-LFCS-92-211. ", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{luo:tver92, author = "Z. Luo", title = "A Unifying Theory of Dependent Types: the schematic approach", journal = "Proc. of Symp. on Logical Foundations of Computer Science (Logic at Tver'92), LNCS 620", year = "1992", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "Also as LFCS Report ECS-LFCS-92-202, Dept. of Computer Science, University of Edinburgh" } @Article{luo:tver92short, author = "Z. Luo", title = "A Unifying Theory of Dependent Types: the schematic approach", journal = "Proc. of Symp. on Logical Foundations of Computer Science (Logic at Tver'92), LNCS 620", year = "1992", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "Also as LFCS Report ECS-LFCS-92-202, Dept. of Computer Science, University of Edinburgh" } @Article{MacQ:module84, author = "D. MacQueen", title = "Modules for standard {ML}", journal = "{ACM} Symp. on Lisp and Functional Programming", year = "1984", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{MacQ:module86, author = "D. MacQueen", title = "Using Dependent Types to Express Modular Structure", journal = "Proc. 13th Principles of Programming Languages", year = "1986", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @TechReport{ReusStreicher:laws92, author = "B. Reus and Th. Streicher", title = "Lifting the laws of module algebra to deliverables", institution = "Ludwig-Maximilians-Universit{\"{a}}t M{\"{u}}nichen, Institut f{\"{u}}r Informatik", year = "1992", OPTtype = "", OPTnumber = "", OPTaddress = "", OPTmonth = "", OPTnote = "" } @MastersThesis{wand:MSc92, author = "P. Wand", title = "Functional Programming and Verification with {Lego}", school = "Department of Computer Science, University of Edinburgh", year = "1992", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{luo:MSCS93, author = "Z. Luo", title = "Program specification and data refinement in type theory", journal = "Mathematical Structures in Computer Science", year = "1993", volume = "3", number = "3", OPTpages = "", OPTmonth = "", OPTnote = "An earlier version appears as \cite{Luo:tapsoft91}" } @Article{luo:MSCS93-only, author = "Z. Luo", title = "Program specification and data refinement in type theory", journal = "Mathematical Structures in Computer Science", year = "1993", volume = "3", number = "3", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{Kolmogorov:32, author = "A.N. Kolmogorov", title = "Zur Deutung der Intuitionistischen Logik", journal = "Math. Z.", year = "1932", volume = "35", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{Ramsey:25, author = "F.P. Ramsey", title = "The Foundations of Mathematics", journal = "Proceedings of the London Mathematical Society", year = "1925", volume = "25", OPTnumber = "", pages = "338-384", OPTmonth = "", OPTnote = "" } @TechReport{HookHowe:paradox, author = "J. Hook and D. Howe", title = "Impredicative Strong Existential Equivalent to {Type:Type}", institution = "Cornell University", year = "1986", type = "Technical Report", number = "TR86-760", OPTaddress = "", OPTmonth = "", OPTnote = "" } @InProceedings{Kreisel:68, author = "G. Kreisel", title = "Functions, Ordinals, Species", booktitle = "Logic, Methodology and Philosophy of Science {III}", year = "1968", editor = "B. {van Rootselaar} and J. Staal", OPTpages = "", OPTorganization = "", publisher = "North-Holland", address = "Amsterdam", OPTmonth = "", OPTnote = "" } @Book{Prawitz:65, author = "D. Prawitz", title = "Natural Deduction, a Proof-Theoretic Study", publisher = "Lmqvist and Wiksell", year = "1965", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Book{Principia, author = "A.N. White and B.A.W. Russell", title = "Principia Mathematica", publisher = "Cambridge University Press", year = "1925", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", edition = "2nd", OPTmonth = "", OPTnote = "" } @Book{Russell:book03, author = "B.A.W. Russell", title = "The Principles of Mathematics", publisher = "Routledge", year = "1903", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", note = "Paperback edition, 1992" } @InProceedings{CoqGal:SN, author = "Th. Coquand and J.H. Gallier", title = "A proof of strong normalization for the theory of constructions using a {Kripke}-like interpretation", booktitle = "Preliminary Proc. of the Workshop on Logical Frameworks", year = "1990", OPTeditor = "", OPTpages = "", OPTorganization = "", OPTpublisher = "", address = "Antibes", OPTmonth = "", OPTnote = "" } @Unpublished{Mog:85, author = "E. Moggi", title = "The {PER}-model as Internal Category with All Small Products", note = "manuscript", year = "1985", OPTmonth = "" } @TechReport{LongoMog:88, author = "G. Longo and E. Moggi", title = "Constructive Natural Deduction and Its `Modest' Interpretation", institution = "Computer Science Dept., Carnegie Mellon Univ.", year = "1988", OPTtype = "", number = "CMU-CS-88-131", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{Seely:86, author = "R.A.G. Seely", title = "Categorical Semantics for Higher-order Polymorphic Lambda Calculus", journal = "J. of Symbolic Logic", year = "1986", volume = "52", number = "4", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{Pitts:87, author = "A. Pitts", title = "Polymorphism is Set Theoretic, Constructively", journal = "Proc. of the Summer Conf. on Category Theory and Computer Science", year = "1987", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "Edinburgh" } @TechReport{Meseguer:88, author = "J. Meseguer", title = "Relating Models of Polymorphism", institution = "Computer Science Lab, SRI International", year = "1988", OPTtype = "", number = "SRI-CSL-88-13", OPTaddress = "", OPTmonth = "", OPTnote = "" } @TechReport{luo:88a, author = "Z. Luo", title = "A Higher-order Calculus and Theory Abstraction", institution = "Dept. of Computer Science, Edinburgh University", year = "1988", type = "LFCS Report", number = "ECS-LFCS-88-57", OPTaddress = "", OPTmonth = "", OPTnote = "" } @TechReport{luo:CCinf, author = "Z. Luo", title = "{CC}$_{\subset}^{\infty}$ and Its Meta Theory", institution = "Dept. of Computer Science, Edinburgh University", year = "1988", type = "LFCS report", number = "ECS-LFCS-88-58", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Book{Levy:book79, author = "A. Levy", title = "Basic Set Theory", publisher = "Springer-Verlag", year = "1979", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Book{Devlin:book79, author = "K. Devlin", title = "Fundamentals of Contemporary Set Theory", publisher = "Springer-Verlag", year = "1979", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Article{SanBur:83, author = "D. Sannella and R. Burstall", title = "Structured Theories in {LCF}", journal = "Proc. of the 8th Colloquium on Trees in Algebra and Programming", year = "1983", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{Zucker:theory75, author = "J. Zucker", title = "Formalization of Classical Mathematics in {AUTOMATH}", journal = "Colloque Internationaux du CNRS, 249", year = "1975", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{Gentzen:35, author = "G. Gentzen", title = "Untersuchungen {\"{u}}ber das logische Schliessen", journal = "Mathematische Zeitschrift", year = "1935", volume = "39", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Book{Carnap:LogicalSyntax, author = "R. Carnap", title = "The Logical Syntax of Language", publisher = "?", year = "1937", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @InCollection{Carnap:logicism30, author = "R. Carnap", title = "The logicist foundations of mathematics", OPTcrossref = "", OPTkey = "", booktitle = "Philosophy of Mathematics: selected readings", publisher = "Cambridge University Press", year = "1983", editor = "P. Benacerraf and H. Putnam", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTtype = "", OPTchapter = "", OPTpages = "", OPTaddress = "", edition = "2", OPTmonth = "", OPTnote = "", OPTannote = "" } @Book{Quine:PhilOfLogic, author = "W.V. Quine", title = "Philosophy of Logic", publisher = "Harvard University Press", year = "1986", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", edition = "second", OPTmonth = "", OPTnote = "" } @InProceedings{Quine:Carnap-and-logical-truth, author = "W.V. Quine", title = "Carnap and logical truth", booktitle = "Logic and Language: Studies Dedicated to Professor Rudolf Carnap", year = "1962", editor = "B. Kazemier and D. Vuysje", OPTpages = "", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Unpublished{coq:pattern-matching92, author = "Th. Coquand", title = "Pattern Matching with Dependent Types", note = "Talk given at the BRA workshop on Proofs and Types, Bastad", year = "1992", OPTmonth = "" } @Article{Klop:80, author = "J. W. Klop", title = "Combinatory Reduction Systems", journal = "Mathematical Center Tracts 127", year = "1980", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{Mitchell:86, author = "J.C. Mitchell", title = "A Type Inference Approach to Reduction Properties and Semantics of Polymorphic Expressions", journal = "Proc. 1986 ACM Symp. on Lisp and Functional Programming", year = "1986", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Proceedings{Troelstra:73a, title = "Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, 344", year = "1973", editor = "A. S. Troelstra", OPTpublisher = "", OPTorganization = "", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Article{Troelstra:73b, author = "A. S. Troelstra", title = "Notes on Intuitionistic Second-order Arithmetic", journal = "Lecture Notes in Mathematics, 337", year = "1973", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{wang-lee:pc93, author = "D. Wang and J. R. Lee", title = "Pictorial Concepts and a Concept Supporting System", journal = "Journal of Visual Languages and Computing", year = "1993", volume = "4", OPTnumber = "", pages = "177--199", OPTmonth = "", OPTnote = "" } @Misc{streicher:newThesis93, author = "T. Streicher", title = "Investigations into intensional type theory", howpublished = "Hablitation Thesis, Ludwig Maximilian Universit{\"{a}}t", year = "1993", OPTmonth = "", OPTnote = "" } @InCollection{barendregt:PTShandbook92, author = "Barendregt, H.P.", title = "Lambda Calculi with Types", OPTcrossref = "", OPTkey = "", booktitle = "Handbook of Logic in Computer Science", publisher = "Clarendon Press", year = "1992", editor = "S. Abramsky and D. Gabbay and T. Maibaum", volume = "2", OPTnumber = "", OPTseries = "", OPTtype = "", OPTchapter = "", OPTpages = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Misc{barendregt:LamWithTypes92, author = "Barendregt, H.P.", title = "Lambda Calculi with Types", howpublished = "In \cite{Handbook:AGM2}", year = "1992", OPTmonth = "", OPTnote = "" } @Book{Handbook:AGM2, author = "S. Abramsky and D. Gabbay and T. Maibaum", title = "Handbook of Logic in Computer Science", publisher = "Clarendon Press", year = "1992", OPTeditor = "", volume = "2", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Book{luo:book94, author = "Z. Luo", title = "{Computation and Reasoning: A Type Theory for Computer Science}", publisher = "Oxford University Press", year = "1994", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @PhdThesis{Mendler:thesis93, author = "M. Mendler", title = "A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification", school = "University of Edinburgh", year = "1993", OPTaddress = "", OPTmonth = "", note = "Also as Report ECS-LFCS-93-255/CST-97-93, Dept. of Computer Science, Edinburgh University" } @TechReport{thorsten:LegoSN, author = "Th. Altenkirch", title = "Brewing Strong Normalization Proofs with {LEGO}", institution = "Dept. of Computer Science, Edinburgh University", year = "1992", type = "LFCS report", number = "ECS-LFCS-92-230", OPTaddress = "", OPTmonth = "", OPTnote = "" } @InProceedings{alti93-snf, author = "Th. Altenkirch", title = "A Formalization of the Strong Normalization Proof for {System F} in {LEGO}", booktitle = "Typed Lambda Calculi and Applications", year = "1993", editor = "M. Bezem, J.F. Groote", series = "LNCS 664" } @InProceedings{alti93-vm, author = "Th. Altenkirch", title = "Yet another Strong Normalization Proof for the {Calculus of Constructions}", booktitle = "Proceedings of the {Vinterm\"otet}", year = "1993", note = "To appear as Chalmers Tech-report" } @PhdThesis{thorsten:thesis-forthcoming, author = "Th. Altenkirch", title = "Constructions, Inductive Types and Strong Normalization", school = "Edinburgh University", year = "", OPTaddress = "", OPTmonth = "", note = "forthcoming" } @PhdThesis{thorsten:thesis, author = "Th. Altenkirch", title = "Constructions, Inductive Types and Strong Normalization", school = "Edinburgh University", year = "1993", OPTaddress = "", OPTmonth = "", OPTnote = "" } @TechReport{martin:case92, author = "M. Hofmann", title = "Formal Development of Functional Programs in Type Theory", institution = "Dept. of Computer Science, Edinburgh University", year = "1992", type = "LFCS report", number = "ECS-LFCS-92-228", OPTaddress = "", OPTmonth = "", note = "submitted to Science of Computer Programming" } @TechReport{martin:case92-only, author = "M. Hofmann", title = "Formal Development of Functional Programs in Type Theory", institution = "Dept. of Computer Science, Edinburgh University", year = "1992", type = "LFCS report", number = "ECS-LFCS-92-228", OPTaddress = "", OPTmonth = "", note = "submitted to Science of Computer Programming" } @InProceedings{burstall:ECCasSpec, author = "R. Burstall", title = "{Extended Calculus of Constructions} as a Specification Language", booktitle = "Mathematics of Program Construction", year = "1993", editor = "R. Bird and C. Morgan", OPTpages = "", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", note = "Invited talk" } @InProceedings{McKinnaPollack93, author = "J. McKinna and R. Pollack", title = "Pure Type Systems Formalized", booktitle = "Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA'93", year = "1993", editor = "M.Bezem and J.F.Groote", pages = "289--305", month = "March", publisher = "Springer-Verlag, LNCS 664" } @article{PollackA, author="Arnon Avron and Furio Honsell and Ian Mason and Robert Pollack", title="Using Typed Lambda Calculus to Implement Formal Systems on a Machine", journal = "Journal of Automated Reasoning", year = "1992", volume = "9", pages = "309-352" } @InProceedings{Pollack92, author = "R. Pollack", title = "Typechecking in Pure Type Systems", booktitle = "Informal Proceedings of the 1992 Workshop on Types for Proofs and Programs, B\aa stad, Sweden", year = "1992", pages = "271-288", month = "June", note = "available by ftp" } @Unpublished{JuttingMcKinnaPollack93, author = "L. van Benthem Jutting and James McKinna and Robert Pollack", title = "Typechecking in Pure Type Systems", note = "submitted for publication", year = "1993" } @PhdThesis{randy:thesis-forthcoming, author = "R. Pollack", title = "Theory of {LEGO}", school = "Edinburgh University", year = "", OPTaddress = "", OPTmonth = "", note = "forthcoming" } @PhdThesis{randy:thesis, author = "R. Pollack", title = "The Theory of {LEGO}: A Proof Checker for the Extended Calculus of Constructions", school = "Edinburgh University", year = "1994", OPTaddress = "", OPTmonth = "", OPTnote = "" } @PhdThesis{randy:thesis-final, author = "R. Pollack", title = "The Theory of {LEGO}: a proof checker for the Extended Calculus of Constructions", school = "Edinburgh University", year = "1994", OPTaddress = "", OPTmonth = "", OPTnote = "forthcoming" } @Article{randy:tactics, author = "R. Pollack", title = "Are tactics feasible?", OPTcrossref = "", OPTkey = "", journal = "2nd Conf. on Typed Lambda Calculi", year = "1995", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @UNPUBLISHED(hofmannstreicher:groupoid, AUTHOR = "Martin Hofmann and Thomas Streicher", TITLE = "{A model of intensional Martin-L\"of type theory in which unicity of identity proofs does not hold}", NOTE = "To be submitted to LICS '94", month = "July", year = "1993" ) @INPROCEEDINGS(hofmann:contin, AUTHOR = "Martin Hofmann", TITLE = "Sound and Complete axiomatisations for call-by-value control operators", BOOKTITLE = "Proceedings of the 5th conference on category theory in Computer Science CTCS, Amsterdam", YEAR = "1993", note = "To appear as a special issue of MSCS" ) @UNPUBLISHED(hofmann:extelim, AUTHOR = "Martin Hofmann", TITLE = "{Elimination of extensionality in Martin-L\"of type theory}", NOTE = "To appear in the proceedings of the workshop on types for proofs and programs, Nijmegen ", month = "June", year = "1993" ) @techreport (HofmannPierce92, author = "Martin Hofmann and Benjamin Pierce" , title = "An Abstract View of Objects and Subtyping (Preliminary Report)", institution = "University of Edinburgh, LFCS" , type = "Technical Report" , number = "ECS-LFCS-92-226" , year = "1992" , note = "submitted to STACS '94, Caen, France" ) @Misc{BurDia93, author = "R. Burstall and R. Diacanescu", title = "Hiding and behaviour: an institutional approach", howpublished = "to appear as invited paper in a Festschrift, Prentice Hall", year = "1993", OPTmonth = "", OPTnote = "" } @Book{LCF:book, author = "M. Gordon and R. Milner and C. Wadsworth", title = "{LCF}: a mechanised logic of computation", publisher = "Springer-Verlag", year = "1979", OPTeditor = "", volume = "78", series = "{LNCS}", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @PhdThesis{IPE:thesis, author = "B. Ritchie", title = "The Design and Implementation of an Interactive Proof Editor", school = "University of Edinburgh", year = "1987", OPTaddress = "", OPTmonth = "", OPTnote = "" } @Book{paulson:ML, author = "L. Paulson", title = "{ML} for the Working Programmer", publisher = "Cambridge University Press", year = "1991", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @TechReport{paulson:Isabelle, author = "L. Paulson", title = "Introduction to {Isabelle}", institution = "Computer Laboratory, Cambridge University", year = "1993", OPTcrossref = "", OPTkey = "", OPTtype = "", number = "280", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{ML:inf, author = "Martin-L{\"{o}}f, P.", title = "Mathematics of infinity", journal = "{COLOG}'88, {Lecture Notes in Computer Science} 417", year = "1990", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @InProceedings{bird:tutorial89, author = "R. Bird", title = "Lectures on constructive functional programming", OPTcrossref = "", OPTkey = "", editor = "M. Broy", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTpages = "", booktitle = "Constructive Methods in Computer Science, {NATO ASI} Series F55", year = "1989", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @InProceedings{bird:lists87, author = "R. Bird", title = "An introduction to the theory of lists", OPTcrossref = "", OPTkey = "", editor = "M. Broy", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTpages = "", booktitle = "Logic of programming and calculi of discrete design, {NATO ASI} Series F36", year = "1987", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @PhdThesis{healf:thesis, author = "H. Goguen", title = "A Typed Operational Semantics for Type Theory", school = "University of Edinburgh", year = "1994", OPTcrossref = "", OPTkey = "", OPTaddress = "", OPTmonth = "", OPTtype = "", OPTnote = "", OPTannote = "" } @InProceedings{ML:analytic-synthetic94, author = "Martin-L{\"{o}}f, P.", title = "Analytic and synthetic judgements in type theory", OPTcrossref = "", OPTkey = "", editor = "P. Parrini", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTpages = "", booktitle = "Kant and Contemporary Epistemology", year = "1994", OPTorganization = "", publisher = "Kluwer Accademic Publishers", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{SalSmi:subset, author = "A. Salvesen and J. Smith", title = "The strength of the subset type in {\ML}'s type theory", OPTcrossref = "", OPTkey = "", journal = "LICS'88", year = "1988", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @TechReport{longo:impredicative, author = "G. Longo", title = "Some aspects of impredicativity", institution = "Department of Computer Science, CMU", year = "1988", OPTcrossref = "", OPTkey = "", type = "Technical report", number = "CMU-CS-88-135", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Unpublished{Wand:strongFP-notes, author = "D. Wand", title = "Elementary strong functional programming", note = "Private communication", OPTcrossref = "", OPTkey = "", year = "1993", OPTmonth = "", OPTannote = "" } @InProceedings{meertens:alg86, author = "L. Meertens", title = "Algorithmics: towards programming as a mathematical activity", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTpages = "", booktitle = "Proc. {CWI} Symp. on Mathematics and Computer Science", year = "1986", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Unpublished{backhouse:bird-meerten88, author = "R. Backhouse", title = "An exploration of the {Bird-Meertens} formalism", note = "manuscript", OPTcrossref = "", OPTkey = "", year = "1988", OPTmonth = "", OPTannote = "" } @Unpublished{luo:generic-programming-in-preparation, author = "Z. Luo", title = "Generic programming and program transformation", note = "In preparation", OPTcrossref = "", OPTkey = "", year = "1994", OPTmonth = "", OPTannote = "" } @Article{FeltyHowe:reuse, author = "A. Felty and D. Howe", title = "Generalisation and reuse of tectic proofs", OPTcrossref = "", OPTkey = "", journal = "Proc. of 5th Inter. Conf. on Logic Programming and Automated Reasoning", year = "1994", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{luo:reuse95, author = "Z. Luo", title = "Developing reuse technology in proof engineering", OPTcrossref = "", OPTkey = "", journal = "Proceedings of AISB95, Workshop on Automated Reasoning: bridging the gap between theory and practice, Sheffield, U.K.", year = "1995", OPTvolume = "", OPTnumber = "", OPTpages = "", month = "April", OPTnote = "", OPTannote = "" } @Article{pollack:TLCA95, author = "R. Pollack", title = "A verified proof checker", OPTcrossref = "", OPTkey = "", journal = "Proceedings of the 2nd Inter. Conf. on Typed Lambda Calculi and Applications, Edinburgh", year = "1995", OPTvolume = "", OPTnumber = "", OPTpages = "", month = "April", OPTnote = "", OPTannote = "" } @Book{roberto:book, author = "D. Long and R. Garigliano", title = "???", publisher = "???", year = "1994", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{bennett:MA92, author = "K. Bennett, T. Bull and H. Yang", title = "A transformation system for maintenance---turning theory into practice", OPTcrossref = "", OPTkey = "", journal = "Proc. of Inter. Conf. on Software Maintenance, Florida", year = "1992", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @TechReport{lego:lib94, author = "C. Jones and S. Maharaj", title = "The {Lego} library", institution = "{LFCS}, Department of Computer Science, University of Edinburgh", year = "1994", OPTcrossref = "", OPTkey = "", OPTtype = "", OPTnumber = "", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @PhdThesis{adriana:thesis, author = "A. Compagnoni", title = "Higher-order Subtyping with Intersection Types", school = "Katholieke Universiteit Nijmegen", year = "1995", OPTcrossref = "", OPTkey = "", OPTaddress = "", OPTmonth = "", OPTtype = "", OPTnote = "", OPTannote = "" } @Article{pfenning:refn-types93, author = "F. Pfenning", title = "Refinement types for logical frameworks", OPTcrossref = "", OPTkey = "", journal = "Preliminary Proceedings of BRA Workshop on Types and Proofs", year = "1993", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{Moh:indCoq, author = "C. Paulin-Mohring", title = "Inductive definitions in the system {Coq}: rules and properties", OPTcrossref = "", OPTkey = "", journal = "Proceedings of the Inter. Conf. on Typed Lambda Calculi and Applications (TLCA'93), LNCS 664", year = "1993", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{healf:TLCA95, author = "H. Goguen", title = "Typed operational semantics", OPTcrossref = "", OPTkey = "", journal = "Proceedings of the 2nd Inter. Conf. on Typed Lambda Calculi and Applications, Edinburgh", year = "1995", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{peterson:ME81, author = "G. L. Peterson", title = "Myths about the mutual exclusion problem", OPTcrossref = "", OPTkey = "", journal = "Information Processing Letters", year = "1981", volume = "12", number = "3", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @TechReport{manna-pnueli:temporal, author = "Z. Manna and A. Pnueli", title = "Verification of concurrent programs (Part {I}, {II}, {III})", institution = "Stanford University", year = "1981", OPTcrossref = "", OPTkey = "", OPTtype = "", OPTnumber = "", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @TechReport{plotkin:oprn-sem, author = "G. Plotkin", title = "A structural approach to operational semantics", institution = "Computer Science Dept, Arhus University", year = "1981", OPTcrossref = "", OPTkey = "", OPTtype = "", number = "DAIMI-FN-19", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @InCollection{stirling:92, author = "C. Stirling", title = "Modal and temporal logics", OPTcrossref = "", OPTkey = "", booktitle = "Handbook of Logic in Computer Science", publisher = "Oxford University Press", year = "1992", editor = "S. Abramsky and D. Gabbay and T. Maibaum", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTtype = "", OPTchapter = "", OPTpages = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{stirling:95, author = "C. Stirling", title = "Modal and temporal logics for processes", OPTcrossref = "", OPTkey = "", OPTbooktitle = "", OPTpublisher = "", year = "1995", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTtype = "", OPTchapter = "", OPTpages = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Book{ben-ari:book90, author = "M. Ben-Ari", title = "Principles of concurrent and distributed programming", publisher = "Prentice-Hall", year = "1990", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{curzon:proof-maintenance95, author = "P. Curzon", title = "The importance of proof maintenance and reengineering", OPTcrossref = "", OPTkey = "", OPTjournal = "", year = "1995", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Book{HOL:book93, author = "M. Gordon and T. Melham", title = "Introduction to {HOL}: a theorem proving environment for higher-order logic", publisher = "Cambridge University Press", year = "1993", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @PhdThesis{martin:thesis, author = "M. Hofmann", title = "Extensional concepts in intensional type theory", school = "Department of Computer Science, University of Edinburgh", year = "1995", OPTcrossref = "", OPTkey = "", OPTaddress = "", OPTmonth = "", OPTtype = "", OPTnote = "", OPTannote = "" } @InProceedings{Dijkstra:semaphore, author = "E.W. Dijkstra", title = "Cooperating sequential processes", OPTcrossref = "", OPTkey = "", editor = "F. Genuys", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTpages = "", booktitle = "Programming Languages", year = "1968", OPTorganization = "", publisher = "Academic Press", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{luo:concurrency-submitted, author = "Z. Luo", title = "Formal verification of concurrent algorithms in type theory", OPTcrossref = "", OPTkey = "", OPTjournal = "", year = "1995", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "Submitted to {TACAS}96 for publication", OPTannote = "" } @Article{BCGS:IC91, author = "V. {Breazu-Tannen} and T. Coquand and C. Gunter and A. Scedrov", title = "Inheritance and explicit coercion", OPTcrossref = "", OPTkey = "", journal = "Information and Computation", year = "1991", volume = "93", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @InProceedings{BCGS:lics89, author = "V. {Breazu-Tannen} and T. Coquand and C. Gunter and A. Scedrov", title = "Inheritance and explicit coercion", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTpages = "", booktitle = "Proc. of LICS'89", year = "1989", OPTorganization = "IEEE", OPTpublisher = "", OPTaddress = "Asilomar, California, U.S.A.", OPTmonth = "", OPTnote = "", OPTannote = "" } @InProceedings{aspinall:singleton94, author = "D. Aspinall", title = "Subtyping with singleton types", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "993", OPTnumber = "", OPTseries = "LNCS", OPTpages = "", booktitle = "CSL'94, LNCS'993", year = "1995", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{courant:singleton02, author = "J. Courant", title = "Strong normalisation with singleton types", OPTcrossref = "", OPTkey = "", journal = "Electronic Notes in Theoretical Computer Science", year = "2002", volume = "70", number = "1", OPTpages = "", OPTmonth = "", OPTnote = "To appear", OPTannote = "" } @Article{aspinall-compagnoni:lics96, author = "D. Aspinall and A. Compagnoni", title = "Subtyping dependent types", OPTcrossref = "", OPTkey = "", journal = "Proc. of {LICS}96", year = "1996", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "To appear", OPTannote = "" } @Misc{Pollack:email, OPTcrossref = "", OPTkey = "", OPTauthor = "R. Pollack", OPTtitle = "", howpublished = "Email communications", year = "1995", OPTmonth = "", OPTnote = "", OPTannote = "" } @InProceedings{plotkin-abadi:LPP93, author = "G. Plotkin and M. Abadi", title = "A logic for parametric polymorphism", OPTcrossref = "", OPTkey = "", editor = "M. Bezem and J. Groote", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTpages = "", booktitle = "Typed Lambda Calculi and Applications, {LNCS} 664", year = "1993", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{plotkin-abadi-cardelli:subpar94, author = "G. Plotkin and M. Abadi and L. Cardelli", title = "Subtyping and parametricity", OPTcrossref = "", OPTkey = "", OPTjournal = "", year = "1994", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{anthony:coercion96, author = "A. Bailey", title = "Lego with implicit coercions", OPTcrossref = "", OPTkey = "", OPTjournal = "", year = "1996", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "Draft", OPTannote = "" } @Article{bruce-longo:subtyping90, author = "K. Bruce and G. Longo", title = "A modest model of records, inheritance, and bounded quantification", OPTcrossref = "", OPTkey = "", journal = "Information and Computation", year = "1990", volume = "87", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @InProceedings{longo-milsted-soloviev:lics95, author = "G. Longo and K. Milsted and S. Soloviev", title = "A logic of subtyping", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTpages = "", booktitle = "Proc. of {LICS'95}", year = "1995", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Book{milner:bookCCS, author = "R. Milner", title = "Communication and Concurrency", publisher = "Prentice Hall", year = "1989", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{luo-yu:draft96, author = "Z. Luo and S. Yu", title = "Model-checking as a proof procedure in type theory", OPTcrossref = "", OPTkey = "", OPTjournal = "", year = "1995", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "Draft", OPTannote = "" } @Unpublished{saibi:popl-draft, author = "A. Sa{\"{i}}bi", title = "Typing algorithm in type theory with inheritance", note = "Draft", OPTcrossref = "", OPTkey = "", year = "1996", OPTmonth = "", OPTannote = "" } @Article{saibi:popl97, author = "A. Sa{\"{i}}bi", title = "Typing algorithm in type theory with inheritance", OPTcrossref = "", OPTkey = "", journal = "POPL'97", year = "1997", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{luo:CSL96, author = "Z. Luo", title = "Coercive subtyping in type theory", OPTcrossref = "", OPTkey = "", journal = "CSL'96, LNCS'1258", year = "1997", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @InCollection{dB:MV94, author = "de Bruijn, N. G.", title = "The mathematical vernacular, a language for mathematics with typed sets", OPTcrossref = "", OPTkey = "", booktitle = "Selected Papers on {Automath}", publisher = "North Holland", year = "1994", editor = "R. P. Nederpelt and J. H. Geuvers and R. C. de Vrijer", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTtype = "", OPTchapter = "", OPTpages = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Book{ranta:book94, author = "A. Ranta", title = "Type-Theoretical Grammar", publisher = "Oxford University Press", year = "1994", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{dowek:undecidability, author = "G. Dowek", title = "The undecidability of typability in the {lambda-Pi} calculus", OPTcrossref = "", OPTkey = "", journal = "Proc of Typed Lambda Calculi and Applications, LNCS 664", year = "1993", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Unpublished{JLS:types96-draft, author = "A. Jones and Z. Luo and S. Soloviev", title = "Some proof-theoretic and algorithmic aspects of coercive subtyping", note = "Draft, submitted for publication", OPTcrossref = "", OPTkey = "", year = "1997", OPTmonth = "", OPTannote = "" } @Article{jls:TYPES96-toappear, author = "A. Jones and Z. Luo and S. Soloviev", title = "Some proof-theoretic and algorithmic aspects of coercive subtyping", OPTcrossref = "", OPTkey = "", journal = "Proc. of the Annual Conf on Types and Proofs (TYPES'96)", year = "1997", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "To appear", OPTannote = "" } @Article{jls:TYPES96, author = "A. Jones and Z. Luo and S. Soloviev", title = "Some proof-theoretic and algorithmic aspects of coercive subtyping", OPTcrossref = "", OPTkey = "", journal = "Types for proofs and programs (eds, E. Gimenez and C. Paulin-Mohring), Proc. of the Inter. Conf. TYPES'96, LNCS 1512", year = "1998", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{ranta:IGPL95, author = "A. Ranta", title = "Type-theoretical interpretation and generalization of phrase structure grammar", OPTcrossref = "", OPTkey = "", journal = "Bulletin of the {IGPL}", year = "1995", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Book{morrill:book94, author = "G. V. Morrill", title = "Type Logical Grammar", publisher = "Kluwer Academic Publishers", year = "1994", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{cardelli:linking97, author = "L. Cardelli", title = "Program fragments, linking, and modularisation", OPTcrossref = "", OPTkey = "", journal = "Proc. of {POPL}97", year = "1997", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{luo:JLC97submitted, author = "Z. Luo", title = "Coercive subtyping", OPTcrossref = "", OPTkey = "", journal = "Submitted to Journal of Logic and Computation", year = "1997", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{luo:JLC97draft, author = "Z. Luo", title = "Coercive subtyping", OPTcrossref = "", OPTkey = "", OPTjournal = "", year = "1997", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "Draft", OPTannote = "" } @Article{luo-callaghan:LACL97-ExtAbs, author = "Z. Luo and P. Callaghan", title = "Linguistic categories in mathematical vernacular and their type-theoretic semantics (extended abstract)", OPTcrossref = "", OPTkey = "", journal = "Logical Aspects of Computational Linguistics 97", year = "1997", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{luo-paul:LACL97-draft, author = "Z. Luo and P. Callaghan", title = "Mathematical vernacular and conceptual well-formedness in mathematical language", OPTcrossref = "", OPTkey = "", journal = "Proc of LACL97.", year = "1998", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "To appear in LNCS series", OPTannote = "" } @Article{luo-paul:LACL97, author = "Z. Luo and P. Callaghan", title = "Mathematical vernacular and conceptual well-formedness in mathematical language", OPTcrossref = "", OPTkey = "", journal = "Proceedings of the 2nd Inter. Conf. on Logical Aspects of Computational Linguistics, {LNCS/LNAI} 1582", year = "1998", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Book{castagna:book, author = "G. Castagna", title = "\hspace{-.05in}Object-Oriented Programming: a Unified Foundation", publisher = "\hspace{-.07in} Birkh{\"{a}}user", year = "\hspace{-.04in}1997", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{Thomas:TAPSOFT97, author = "Thomas Schreiber", title = "Auxiliary Variables and Recursive Procedures", OPTcrossref = "", OPTkey = "", journal = "TAPSOFT'97: Theory and Practice of Software Development, {LNCS} 1214", year = "1997", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{yu-luo:FME97, author = "S. Yu and Z. Luo", title = "Implementing a model checker for {Lego}", OPTcrossref = "", OPTkey = "", journal = "Proc. of the 4th Inter Symp. of Formal Methods Europe, FME'97: Industrial Applications and Strengthened Foundations of Formal Methods, Graz, Austria. {LNCS} 1313", year = "1997", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{luo:LC96, author = "Z. Luo", title = "Logical truths in constructive type theory (abstract)", OPTcrossref = "", OPTkey = "", journal = "Logic Colloquium 96", year = "1996", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{bylands:95, author = "T. Bull and E. Younger and K. Bennett and Z. Luo", title = "Bylands: reverse engineering safety-critical systems", OPTcrossref = "", OPTkey = "", journal = "Proc. of Inter. Conf. on Software Maintenance", year = "1995", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{bylands:96, author = "E. Younger and Z. Luo and K. Bennett and T. Bull", title = "Reverse engineering concurrent programs using formal modelling and analysis", OPTcrossref = "", OPTkey = "", journal = "Proc of IEEE Inter. Conf. on Software Maintenance", year = "1996", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{bylands:97, author = "E. Younger and K. Bennett and Z. Luo", title = "A formal transformation and refinement method for re-engineering concurrent programs", OPTcrossref = "", OPTkey = "", journal = "Proc of IEEE Inter. Conf. on Software Maintenance", year = "1997", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{luo:JLC97-accepted, author = "Z. Luo", title = "Coercive subtyping", OPTcrossref = "", OPTkey = "", journal = "Journal of Logic and Computation", year = "1997", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "Accepted, to appear in 1998", OPTannote = "" } @Article{luo:JLC98-toappear, author = "Z. Luo", title = "Coercive subtyping", OPTcrossref = "", OPTkey = "", journal = "Journal of Logic and Computation", year = "1998", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "To appear", OPTannote = "" } @Article{luo:JLC99, author = "Z. Luo", title = "Coercive subtyping", OPTcrossref = "", OPTkey = "", journal = "J of Logic and Computation", year = "1999", volume = "9", number = "1", OPTpages = "105-130", OPTmonth = "", OPTnote = "", OPTannote = "" } @PhdThesis{anthony:thesis, author = "A. Bailey", title = "The Machine-checked Literate Formalisation of Algebra in Type Theory", school = "University of Manchester", year = "1999", OPTcrossref = "", OPTkey = "", OPTaddress = "", OPTmonth = "", OPTtype = "", OPTnote = "Forthcoming", OPTannote = "" } @PhdThesis{anthony:thesis-forthcoming, author = "A. Bailey", title = "The Machine-checked Literate Formalisation of Algebra in Type Theory", school = "University of Manchester", year = "1998", OPTcrossref = "", OPTkey = "", OPTaddress = "", OPTmonth = "", OPTtype = "", note = "Forthcoming", OPTannote = "" } @Proceedings{Durham:workshop97, title = "Proc of TYPES Working Group Workshop on Subtyping, Inheritance, and Modularisation of Proofs", year = "1997", OPTcrossref = "", OPTkey = "", editor = "Z. Luo and S. Soloviev", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTpublisher = "", OPTorganization = "", address = "Durham", OPTmonth = "", OPTnote = "", OPTannote = "" } @Unpublished{luo:ESSLLI97-old, author = "Z. Luo", title = "Mathematical Vernacular", note = "Invited talk at the ESSILLI Workshop on Informal Mathematical Languages", OPTcrossref = "", OPTkey = "", year = "1997", OPTmonth = "", OPTannote = "" } @Unpublished{luo:ESSLLI97, author = "Z. Luo and P. Callaghan", title = "Designing a Mathematical Vernacular", note = "Invited talk at the European Summer School in Logic, Language, and Information (ESSLLI'97) Workshop on Informal Mathematical Languages", year = "1997", OPTannote = "" } @Unpublished{luo:summer-school95, author = "Z. Luo", title = "Formalisation of concurrent programs in type theory", note = "Lecture notes for the Lego Summer School, Germany", OPTcrossref = "", OPTkey = "", year = "1995", OPTmonth = "", OPTannote = "" } @PhdThesis{yu:thesis-draft, author = "S. Yu", title = "Formal veirifcation of concurrent programs in type theory", school = "University of Durham", year = "1998", OPTcrossref = "", OPTkey = "", OPTaddress = "", OPTmonth = "", OPTtype = "", note = "Draft", OPTannote = "" } @Unpublished{yu-luo:FAC-draft, author = "S. Yu and Z. Luo", title = "A verification environment based on type theory", note = "Submitted to Journal of Formal Aspects of Computing", OPTcrossref = "", OPTkey = "", year = "1998", OPTmonth = "", OPTannote = "" } @Unpublished{yu:imperative-draft, author = "S. Yu", title = "A verification environment for imperative programs", note = "Draft paper for TYPES'97", OPTcrossref = "", OPTkey = "", year = "1998", OPTmonth = "", OPTannote = "" } @Unpublished{maria:planning-draft, author = "M. Fox and D. Long", title = "Formalising non-linear planning", note = "Manuscript submitted for publication", OPTcrossref = "", OPTkey = "", year = "1997", OPTmonth = "", OPTannote = "" } @Article{shiu-luo-garigliano:FAPR96, author = "S. Shiu and Z. Luo and R. Garigliano", title = "Type-theoretic semantics for SemNet", OPTcrossref = "", OPTkey = "", journal = "Proc. of Inter. Conf. on Formal and Applied Practical Reasoning, LNAI 1085", year = "1996", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Book{Lincoln:Book, author = "L. Wallen", title = "Automated Proof Search in Non-classical Logics", publisher = "MIT", year = "1990", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @TechReport{dyckhoff:mutation-free, author = "R. Dyckhoff and L. Pinto", title = "A permutation-free sequent calculus for intuitionistic logic ", institution = "Computer Science Division, St Andrews University", year = "1996", OPTcrossref = "", OPTkey = "", OPTtype = "", number = "CS/96/9", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{harrison:BDD, author = "J. Harrison", title = "Binary Decision Diagrams as a HOL Derived Rule", OPTcrossref = "", OPTkey = "", journal = "The Computer Journal", year = "1995", volume = "38", number = "1", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{comp:lics94, author = "H. Andersen and C. Stirling and G. Winskel", title = "A compositional proof system for modal $\mu$-calculus", OPTcrossref = "", OPTkey = "", journal = "LICS", year = "1994", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Book{MannaPnueli:book95, author = "Z. Manna and A. Pnueli", title = "Temporal Verification of Reactive Systems: Safety", publisher = "Sringer-Verlag", year = "1995", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{dedMC:cav96, author = "H. Sipma and T. Uribe and Z. Manna", title = "Deductive model checking", OPTcrossref = "", OPTkey = "", journal = "Proc. Inter. Conf. on Computer Aided Verification (CAV'96)", year = "1996", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{BDD:86, author = "R. Bryant", title = "Graph-based algorithms for Boolean function manipulation", OPTcrossref = "", OPTkey = "", journal = "IEEE Trans. on Computers", year = "1986", volume = "35", number = "8", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{Clarke:abstraction92, author = "E. Clarke and O. Grunmberg and D. Long", title = "Model-checking and abstraction", OPTcrossref = "", OPTkey = "", journal = "Proc of 19th Ann. ACM Symp on Principles of Programming Languages (POPL'92)", year = "1992", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{Jackson:abstraction94, author = "D. Jackson", title = "Abstract model-checking of infinite specifications", OPTcrossref = "", OPTkey = "", journal = "Proc of Formal Methods Europe (FME'94)", year = "1994", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{protocol:coq, author = "L. Helmink and M. Sellink and F. Vaandrager", title = "Proof-checking a data link protocol", OPTcrossref = "", OPTkey = "", journal = "TYPES'94", year = "1994", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{protocol:PVS, author = "K. Haveland and N. Shankar", title = "Experiments in theorem proving and model checking for protocol verification", OPTcrossref = "", OPTkey = "", journal = "Proc Formal Methods Europe FME'96", year = "1996", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @TechReport{Bou96, author = "R. Boulton", title = "A tool to support formal reasoning about computer languages", institution = "Computer Lab, Univ of Cambridge", year = "1996", OPTcrossref = "", OPTkey = "", OPTtype = "", number = "TR405", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{pollack:theory, author = "R. Pollack", title = "Theories in Type Theory ", OPTcrossref = "", OPTkey = "", journal = "In \cite{Durham:workshop97}", year = "1997", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @InProceedings{pollack:belief, author = "R. Pollack", title = "How to Believe a Machine-Checked Proof,", OPTcrossref = "", OPTkey = "", editor = "G. Sambin and J. Smith", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTpages = "", booktitle = "Twenty-Five Years of Constructive Type Theory", year = "1997", OPTorganization = "", publisher = "Oxford University Press", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{courant:TLCA97, author = "J. Courant", title = "A module system for Pure Type Systems", OPTcrossref = "", OPTkey = "", journal = "Proc of TLCA'97", year = "1997", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{InfMC, author = "J. Bradfield and C. Stirling", title = "Local model checking for infinite state spaces", OPTcrossref = "", OPTkey = "", journal = "Theoretical Computer Science", year = "1992", volume = "96", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @TechReport{pointing, author = "Y. Bertot and T. Kleymann-Schreiber and D. Sequeira", title = "Implementing Proof by Pointing without a Structure Editor", institution = "Dept of Computer Science, University of Edinburgh", year = "1997", OPTcrossref = "", OPTkey = "", OPTtype = "", number = "ECS-LFCS-97-368", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Book{agent:book95, author = "M. Wooldridge and N. Jennings (eds.)", title = "Intelligent Agents -- Theories, Architectures, and Languages, LNAI 890", publisher = "Sringer-Verlag", year = "1995", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @TechReport{sergei-luo:meta98, author = "S. Soloviev and Z. Luo", title = "Meta-theoretic study of coercive subtyping", institution = "CS Dept, Durham", year = "1998", OPTcrossref = "", OPTkey = "", OPTtype = "", OPTnumber = "", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Book{jackendoff:book97, author = "R. Jackendoff", title = "{The Architecture of the Language Faculty}", publisher = "MIT", year = "1997", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Book{pustejovsky:book95, author = "J. Pustejovsky", title = "{The Generative Lexicon}", publisher = "MIT", year = "1995", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Book{Lyons:book, author = "J. Lyons", title = "Linguistic Semantics", publisher = "Cambridge University Press", year = "1995", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @MastersThesis{alexjones:msc, AUTHOR="A. Jones", TITLE="The Formalization of Linear Algebra in LEGO: The Decidable Dependency Theorem", SCHOOL="University of Manchester", YEAR="1995" } @Article{ranta:syncat95, author = "A. Ranta", title = "Syntactic categories in the language of mathematics", OPTcrossref = "", OPTkey = "", journal = "LNCS 996", year = "1995", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{barthes:TYPES95, author = "G. Barthe", title = "Implicit coercions in type systems", OPTcrossref = "", OPTkey = "", journal = "Proceedings of Types'95, LNCS 1128", year = "1996", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @InProceedings{bet-tar:subtyping98, author = {G. Betarte and A. Tasistro}, title = {Extension of {\ML}'s type theory with record types and subtyping}, booktitle = {Twenty-five Years of Constructive Type Theory}, OPTcrossref = {}, OPTkey = {}, OPTpages = {}, year = {1998}, editor = {G. Sambin and J. Smith}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, publisher = {Oxford University Press}, OPTnote = {}, OPTannote = {} } @PhdThesis{tasistro:thesis, author = "A. Tasistro", title = "Substitution, record types and subtyping in type theory", school = "Chalmers University of Technology", year = "1997", OPTcrossref = "", OPTkey = "", OPTaddress = "", OPTmonth = "", OPTtype = "", OPTnote = "", OPTannote = "" } @Article{paul-luo:cluk98-draft, author = "P. Callaghan and Z. Luo", title = "Computer-assisted reasoning with natural language: implementing a mathematical vernacular", OPTcrossref = "", OPTkey = "", OPTjournal = "", year = "1998", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "Draft paper submitted", OPTannote = "" } @Article{turner:ESFP95, author = "D. Turner", title = "Elementary Strong Functional Programming", OPTcrossref = "", OPTkey = "", journal = "Proceedings of the first international symposium on Functional Programming Languages in Education, {LNCS} 1022", year = "1995", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Unpublished{luo:SFPnotes94, author = "Z. Luo", title = "Algorithm refinement in type theory", note = "manuscript", OPTcrossref = "", OPTkey = "", year = "1994", month = "September", OPTannote = "" } @Unpublished{sergei-luo:TYPES98-draft, author = "S. Soloviev and Z. Luo", title = "Coercion completion and conservativity in coercive subtyping", note = "Talk given at and paper submitted to TYPES'98", OPTcrossref = "", OPTkey = "", year = "1998", OPTmonth = "", OPTannote = "" } @Unpublished{sergei-luo:TYPES98-talk, author = "S. Soloviev and Z. Luo", title = "Coercion completion and conservativity in coercive subtyping", note = "Talk given at TYPES'98", OPTcrossref = "", OPTkey = "", year = "1998", OPTmonth = "", OPTannote = "" } @Unpublished{sergei-luo:meta-draft, author = "S. Soloviev and Z. Luo", title = "Coercion completion and conservativity in coercive subtyping", note = "Draft", OPTcrossref = "", OPTkey = "", year = "1999", OPTmonth = "", OPTannote = "" } @Unpublished{sergei-luo:meta-APALaccepted, author = "S. Soloviev and Z. Luo", title = "Coercion completion and conservativity in coercive subtyping", note = "Annals of Pure and Applied Logic", OPTcrossref = "", OPTkey = "", year = "2001", OPTmonth = "", annote = "In press" } @Unpublished{sergei-luo:journal-draft, author = "S. Soloviev and Z. Luo", title = "Coercive subtyping: coherence and conservativity", note = "Draft paper", OPTcrossref = "", OPTkey = "", year = "1998", OPTmonth = "", OPTannote = "" } @Article{luo-paul:LACL98abstract, author = "Z. Luo and P. Callaghan", title = "Coercive subtyping and lexical semantics (extended abstract)", OPTcrossref = "", OPTkey = "", journal = "Logical Aspects of Computational Linguistics (LACL'98)", year = "1998", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Unpublished{paul:TYPES99, author = "P. C. Callaghan", title = "An implementation of typed {LF} with coercions", note = "The Annual Meeting of TYPES, 1999", OPTcrossref = "", OPTkey = "", year = "1999", OPTmonth = "", OPTannote = "" } @Misc{luo:notes-dep-coercions98, OPTcrossref = "", OPTkey = "", author = "Z. Luo", title = "Dependent coercions", OPThowpublished = "", year = "1998", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{luo-soloviev:CTCS99, author = "Z. Luo and S. Soloviev", title = "Dependent coercions", OPTcrossref = "", OPTkey = "", journal = "CTCS'99, ENTCS'29", year = "1999", OPTvolume = "29", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{luo-soloviev:CTCS99andTCSsubmitted, author = "Z. Luo and S. Soloviev", title = "Dependent coercions", OPTcrossref = "", OPTkey = "", journal = "The 8th Inter. Conf. on Category Theory and Computer Science (CTCS'99), Edinburgh, Scotland. Electronic Notes in Theoretical Computer Science", year = "1999", volume = "29", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "Revised version submitted to Theoretical Computer Science", OPTannote = "" } @Article{paul-luo:UITP98, author = "P. Callaghan and Z. Luo", title = "Mathematical vernacular in type theory based proof assistants", OPTcrossref = "", OPTkey = "", journal = "User Interfaces for Theorem Provers (UITP'98), Eindhoven", year = "1998", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @PhdThesis{ChenGang:thesis, author = "G. Chen", title = "Subtyping, Type Conversion and Transitivity Elimination", school = "University of Paris {VII}", year = "1998", OPTcrossref = "", OPTkey = "", OPTaddress = "", OPTmonth = "", OPTtype = "", OPTnote = "", OPTannote = "" } @Misc{luo:talkTYPES99, OPTcrossref = "", OPTkey = "", author = "R. Kiessling and Z. Luo and J. M. McKinna", title = "Some issues in functional programming with dependent types", howpublished = "Talk in the Annual Conference of TYPES'99", year = "1999", month = "June", OPTnote = "", OPTannote = "" } @Misc{paul:talkTYPES99, OPTcrossref = "", OPTkey = "", author = "P.C. Callaghan", title = "Plastic: an implementation of typed {LF} with coercions", howpublished = "Talk given in the Annual Conf of TYPES'99", year = "1999", month = "June", OPTnote = "", OPTannote = "" } @PhdThesis{conor:thesis-forthcoming, author = "C. McBride", title = "", school = "University of Edinburgh", year = "1999", OPTcrossref = "", OPTkey = "", OPTaddress = "", OPTmonth = "", OPTtype = "", note = "Forthcoming", OPTannote = "" } @PhdThesis{shenwei:thesis-forthcoming, author = "S. Yu", title = "Verification of Concurrent Programs Based on Type Theory", school = "University of Durham", year = "1999", OPTcrossref = "", OPTkey = "", OPTaddress = "", OPTmonth = "", OPTtype = "", note = "Forthcoming", OPTannote = "" } @Article{healf:UTTmeta, author = "H. Goguen", title = "The metatheory of {UTT}", OPTcrossref = "", OPTkey = "", journal = "Types for proofs and programs, {LNCS} 996", year = "1995", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{healf:TLCA99, author = "H. Goguen", title = "Soundness of typed operational semantics for the logical framework", OPTcrossref = "", OPTkey = "", journal = "Typed Lambda Calculi and Applications (TLCA'99)", year = "1999", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{james-randy:JAR-forthcoming, author = "J. H. McKinna and R. Pollack", title = "Some Lambda Calculus and Type Theory Formalized", OPTcrossref = "", OPTkey = "", journal = "Journal of Automated Reasoning", year = "1999", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "Forthcoming", OPTannote = "" } @PhdThesis{thomas:thesis, author = "Th. Kleymann", title = "Hoare Logic and {VDM}: Machine-checked soundness and completeness proofs", school = "University of Ediburgh", year = "1998", OPTcrossref = "", OPTkey = "", OPTaddress = "", OPTmonth = "", OPTtype = "", OPTnote = "", OPTannote = "" } @PhdThesis{reus:thesis, author = "B. Reus", title = "Program Verification in Synthetic Domain Theory", school = "{LMU} Munich", year = "1995", OPTcrossref = "", OPTkey = "", OPTaddress = "", OPTmonth = "", OPTtype = "", OPTnote = "", OPTannote = "" } @Misc{luo:lam-free97, OPTcrossref = "", OPTkey = "", author = "Z. Luo", title = "${\mbox{\sc PAL}}^+$: a lambda-free logical framework", OPThowpublished = "", year = "1997", month = "November", OPTnote = "", OPTannote = "" } @Misc{luo:lam-free00Accepted, OPTcrossref = "", OPTkey = "", author = "Z. Luo", title = "${\mbox{\sc PAL}}^+$: a lambda-free logical framework", OPThowpublished = "", year = "2000", OPTmonth = "", note = "Accepted and to appear in Proc of Workshop on Logical Frameworks and Meta-languages (LFM'2000)", OPTannote = "" } @Misc{luo:lam-free00Accepted-JFP, OPTcrossref = "", OPTkey = "", author = "Z. Luo", title = "${\mbox{\sc PAL}}^+$: a lambda-free logical framework", howpublished = "J. of Functional Programming", year = "2001", OPTmonth = "", note = "Accepted and to appear", OPTannote = "" } @Misc{luo:LFM00, OPTcrossref = "", OPTkey = "", author = "Z. Luo", title = "${\mbox{\sc PAL}}^+$: a lambda-free logical framework", howpublished = "Proc. of Inter Workshop on Logical Frameworks and Meta-languages (LFM'2000), Santa Barbara, California", year = "2000", OPTmonth = "", OPTnote = "", OPTannote = "" } @Misc{luo:meta-var, OPTcrossref = "", OPTkey = "", author = "Z. Luo", title = "Meta-variables and existential judgements", howpublished = "Notes", year = "1997", month = "August", OPTnote = "", OPTannote = "" } @Misc{callaghan-luo:Plastic, OPTcrossref = "", OPTkey = "", author = "P. C. Callaghan and Z. Luo", title = "Plastic: an Implementation of Typed {LF} with Coercive Subtyping and Universes", howpublished = "Submitted to J. of Automated Reasoning, special issue on Logical Frameworks", year = "2000", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{paul-luo:JAR00, author = "P. Callaghan and Z. Luo", title = "An Implementation of {LF} with Coercive Subtyping and Universes. ", OPTcrossref = "", OPTkey = "", journal = "Journal of Automated Reasoning", year = "2001", volume = "27", number = "1", OPTpages = "3-27", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{KM71, author = "G.M. Kelly and S. Mac Lane", title = "Coherence in Closed Categories", OPTcrossref = "", OPTkey = "", journal = "J. Pure and Applied Algebra", year = "1971", OPTvolume = "1", OPTnumber = "1", OPTpages = "97-140", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{M76, author = "S. Mac Lane", title = "Topology and Logic as a Source of Algebra", OPTcrossref = "", OPTkey = "", journal = "Bull. Amer. Math. Soc.", year = "1976", OPTvolume = "82", OPTnumber = "1", OPTpages = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Misc{paul:SubtypingWkshopAccepted, OPTcrossref = "", OPTkey = "", author = "P. C. Callaghan", title = "Coherence checking and its implementation in Plastic", howpublished = "APPSEM Workshop on Subtyping and Dependent Types in Programming", year = "2000", OPTmonth = "", note = "Accepted and to appear", OPTannote = "" } @Article{sergeilongo:coherenceAccepted, author = "G. Longo and K. Milsted and S. Soloviev", title = "Coherence and Transitivity of Subtyping as Entailment", OPTcrossref = "", OPTkey = "", journal = "Journal of Logic and Computation", year = "1999", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "Accpeted and to appear", OPTannote = "" } @Article{sergeilongo:coherence, author = "G. Longo and K. Milsted and S. Soloviev", title = "Coherence and Transitivity of Subtyping as Entailment", OPTcrossref = "", OPTkey = "", journal = "Journal of Logic and Computation", year = "1999", volume = "10", number = "4", pages = "493-526", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{pcc-luo:impl-indtyAccepted, author = "P. Callaghan and Z. Luo", title = "Implementation Techniques for Inductive Types", OPTcrossref = "", OPTkey = "", journal = "Proceedings of TYPES'99", year = "1999", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", note = "Accepted and to appear in LNCS series", OPTannote = "" } @Article{severi-poll:PTSdefn, author = {P. Severi and E. Poll}, title = {Pure type systems with definitions}, journal = {Proc. of {LFCS}'94, {LNCS} 813}, year = {1994}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{paul-luo-pang:object, author = {P. C. Callaghan and Z. Luo and J. Pang}, title = {Object languages in a type-theoretic meta-framework}, journal = {Workshop of Proof Transformation and Presentation and Proof Complexities (PTP'01)}, year = {2001}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @PhdThesis{chen:thesis, author = {G. Chen}, title = {Subtyping, Type Conversion and Transitivity Elimination}, school = {University of Paris {VII}}, year = {1998}, OPTkey = {}, OPTtype = {}, OPTaddress = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Unpublished{yong-sergei-luo:weakinpreparation, author = {Y. Luo and Z. Luo and S. Soloviev}, title = {Weak transitivity in coercive subtyping}, note = {In preparation}, OPTkey = {}, OPTmonth = {}, year = {2001}, OPTannote = {} } @Article{callaghan-luo-pang:workshop01, author = {P. C. Callaghan and Z. Luo and J. Pang}, title = {Object languages in a type-theoretic meta-framework}, journal = {Workshop of Proof Transformation and Presentation and Proof Complexities (PTP'01), Siena, Italy}, year = {2001}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{PVS, author = {S. Owre and J. Rushby and N. Shankar and F. von Henke}, title = {Formal verification fomr fault-tolerant architectures: Prolegomena to the design of {PVS}}, journal = {IEEE Trans. on Soft. Eng.}, year = {1995}, OPTkey = {}, volume = {21}, number = {2}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{OpenMath, author = {Openmath Consortium}, title = {The OpenMath Standard}, journal = {OpenMath Deliverable 1.3.3a}, year = {1999}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{MathML, author = {S. Buswell and others}, title = {Mathematical Markup Language ({MathML}) Specification}, journal = {http://www.w3.org/TR/REC-MathML/}, year = {1999}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @InProceedings{Mathpert1, author = {M. Beeson}, title = {Design Principles of Mathpert: Software to support education in algebra and calculus}, booktitle = {Human Interfaces to Symbolic Computation}, OPTcrossref = {}, OPTkey = {}, OPTpages = {}, year = {1996}, editor = {Kajler, N}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, publisher = {Springer-Verlag}, OPTnote = {}, OPTannote = {} } @Article{Mathpert2, author = {M. Beeson}, title = {Mathpert: Computer support for learning algebra, trigonometry, and calculus}, journal = {Logic Programming and Automated Reasoning, Lecture Notes in Computer Science 624}, year = {1992}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @InProceedings{FTA-TYPES, author = {H. Geuvers and F. Wiedijk and J. Zwanenburg}, title = {A constructive proof of the Fundamental theorem of algebra without using the rationals}, booktitle = {Proc. of TYPES'2000}, OPTcrossref = {}, OPTkey = {}, OPTpages = {}, year = {2001}, editor = {P. Callaghan and Z. Luo and J. McKinna and R. Pollack}, OPTvolume = {}, OPTnumber = {}, series = {LNCS}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, note = {To appear}, OPTannote = {} } @Article{munoz, author = {C. Munoz}, title = {Proof-term synthesis on dependent-type systems via explicit substitutions}, journal = {Theoretical Computer Science}, year = {2001}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{79, author = {P. Aczel}, title = {The Type Theoretic Interpretation of Constructive Set Theory}, journal = {In A. MacIntyre and L. Pacholski, editors, {\it Logic Colloquium '77}}, year = {1979}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, pages = {55--66}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{80a, author = {P. Aczel}, title = {Frege Structures and the notions of Proposition, Truth and Set}, journal = {In H.J.~Keisler J.~Barwise and K. Kunen, editors, {\it Proceedings of the Kleene Symposium}}, year = {1980}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, pages = {31--59}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{82, author = {P. Aczel}, title = {The Type Theoretic Interpretation of Constructive Set Theory: Choice Principles}, journal = {In A.S. Troelstra and D. van~Dalen, editors, {\it Proceedings of the L.E.J. Brouwer Centenary Symposium}, pages~1--40, North Holland}, year = {1982}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{86, author = {P. Aczel}, title = {The Type Theoretic Interpretation of Constructive Set Theory: Inductive Definitions}, journal = {In George~J.W.~Dorn Ruth~Barcan~Marcus and Paul Weingartner, editors, Logic, Methodology and Philosophy of Science VII, Proceedings of the Seventh International Congress, Salzburg, 1983}, year = {1986}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, pages = {17--49}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @BOOK(88, AUTHOR = "P. Aczel", EDITOR = "", TITLE = "Non-Well-Founded Sets", PUBLISHER = "CSLI Lecture Notes, Number 14, Stanford Universit", YEAR = "1988", MONTH = "", EDITION = "", NOTE = "", REVIEW = "") @Article{88c, author = {P. Aczel and P.F.~Mendler}, title = {The notion of a Framework and a framework for {LTC}}, journal = {Proceedings of the 3rd Symposium on Logic in Computer Science, pages 392-399, IEEE}, year = {1988}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{89, author = {P. Aczel and P.F.~Mendler}, title = {A Final Coalgebra Theorem}, journal = {{\it Proceedings of the 1989 Summer Conference on Category Theory and Computer Science}, Springer Lecture Notes in Computer Science vol.389}, year = {1989}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{90, author = {P. Aczel and ~D.~Carlisle}, title = {The Logical Theory of Constructions: A formal framework and its implementation}, journal = {{\it Proceedings of the first workshop on Logical Frameworks}, edited by G. Huet and G. Plotki}, year = {1990}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{90a, author = {P. Aczel}, title = {Replacement Systems and the Axiomatisation of Situation Theory}, journal = {{\it Situation Theory and its Applications, Vol 1}, edited by R. Cooper et al., CSLI Lecture Notes No. 22, Stanford University}, year = {1990}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{91c, author = {P. Aczel and D. Carlisle and N. Mendler}, title = {Two frameworks of theories and their implementation in Isabelle}, journal = {{\it Logical Frameworks}, The Proceedings of the first international workshop on Logical Frameworks, edited by Gerard Huet and Gordon Plotkin}, year = {1991}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{94a, author = {P. Aczel}, title = { Final Universes of Processes}, journal = {{\it Mathematical Foundations of Programming Semantics}, the proceedings of the 9th International Conference, 1993, edited by S. Brookes, M. Main, A. Melton, M. Mislove and D. Schmidt, Springer Lecture Notes in Computer Science, Vol 802}, year = {1994}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{galois94, author = {P. Aczel}, title = {Galois: A Theory Development Project}, journal = {Report, for the Turin meeting on the Representation of Mathematics in Logical Frameworks}, year = {1993}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, note = {\verb+http://cs.man.ac.uk/~petera/galois.ps.gz+}, OPTannote = {} } @Article{galois97, author = { P. Aczel}, title = {A direct constructive treatment of the Fundamental Theorem of Galois Theory}, journal = {Unpublished Report, Manchester}, year = {1997}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, note = {\verb+http://cs.man.ac.uk/~petera/ftgt.ps.gz+}, OPTannote = {} } @Article{96, author = { P. Aczel}, title = {Generalised Set Theory}, journal = {{\it Logic, Language and Computation, Vol 1}, edited by Jerry Seligman and Dag Westerstahl, \newblock the proceedings of the First International Conference, CSLI Lecture Notes No. 58, Stanford University, ISBN No: 1-881-526-909}, year = {1996}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{99a, author = {P. Aczel}, title = {On relating type theories and set theories}, journal = {{\it Types `98}, the proceedings of the 1998 workshop on Types for Proofs and Programs, at Kloster Irsee, edited by T. Altenkirch, W. Naraschewski and B. Reus, \newblock Springer Lecture Notes in Computer Science, LNCS 1657}, year = {1999}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } \bibitem{02} P. Aczel and N.~Gambino. \newblock{ Collection Principles in Dependent Type Theory}, to appear in the proceedings of Types00, (2002). @Article{02, author = {P. Aczel and N.~Gambino}, title = { Collection Principles in Dependent Type Theory}, journal = {Proceedings of Types00}, year = {2002}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, note = {To appear}, OPTannote = {} } @Article{bailey98, author = { A. Bailey}, title = {Coercion Synthesis in computer implementations of type theoretic frameworks}, journal = { {\it Proceedings of TYPES'97} , edited by C. Paulin and E. Gimenez, Springer Lecture Notes in Computer Science, Vol 1512}, year = {1998}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Misc{henk-et-al:FTA, OPTkey = {}, author = {H. Barendregt and others}, title = {{The "Fundamental Theorem of Algebra" Project} web page}, howpublished = {\verb+http://www.cs.kun.nl/~freek/fta/index.html+}, OPTmonth = {}, OPTyear = {}, OPTnote = {}, OPTannote = {} } @Article{LL01, author = {Y. Luo and Z. Luo}, title = {Coherence and transitivity in coercive subtyping}, journal = {Proc. of the 8th Inter. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'01), Havana, Cuba. LNAI 2250}, year = {2001}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{LLS02, author = {Y. Luo and Z. Luo and S. Soloviev}, title = {Weak transitivity in coercive suibtyping}, journal = {Submitted}, year = {2002}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{sergei-luo:APAL, author = {S. Soloviev and Z. Luo}, title = {Coercion completion and conservativity in coercive subtyping}, journal = {Annals of Pure and Applied Logic}, year = {2002}, OPTkey = {}, volume = {113}, number = {1-3}, OPTpages = {297-322}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @InProceedings{Yong-Zhaohui-Sergei:WTT, author = "Y. Luo and Z. Luo and S. Soloviev", title = "Weak Transitivity in Coercive Subtyping", booktitle = "Types for Proofs and Programs", year = "2002", editor = "H. Geuvers and F. Wiedijk", publisher = "Springer-Verlag", isbn = "ISBN 3-540-14031-X", series = "LNCS", pages = "220--239", volume = "2646" } @Book{Bertot:book04, author = "Y. Bertot and P. Casteran", title = "Interactive Theorem Proving and Program Development", publisher = "Springer-Verlag", year = "2004", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Misc{Gon05, OPTcrossref = "", OPTkey = "", author = "G. Gonthier", title = "A computer checked proof of the Four Colour Theorem", OPThowpublished = "", year = "2005", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{GPWZ02, author = {H. Geuvers and others}, title = {A constructive algebraic hierarchy in {Coq} }, journal = {J of Symbolic Computation}, year = {2002}, OPTkey = {}, volume = {34}, number = {4}, OPTpages = {271-286}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Book{Weyl:1918, author = "H. Weyl", title = "The Continuum: a critical examination of the foundation of analysis", publisher = "Dover Publ. 1994", year = "(English translation of Das Kontinuum, 1918)", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Article{AG02, author = {P. Aczel and N. Gambino}, title = {Collection Principles in Dependent Type Theory}, year = {2002}, OPTkey = {}, volume = {Proofs and Programs, (eds) P.Callaghan, Z. Luo, J. McKinna and R. Pollack. LNCS 2277}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{GA06, author = {N. Gambino and P. Aczel}, title = {The generalised type-theoretic interpretation of constructive set theory}, journal = {J. of Symbolic Logic}, year = {2006}, OPTkey = {}, volume = {71}, number = {1}, pages = {67-103}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @InProceedings{Fef05, author = "S. Feferman", title = "Predicativity", booktitle = "The Oxford Handbook of Philosophy of Mathematics and Logic", year = "2005", editor = "S. Shapiro", publisher = "Oxford Univ Press", OPTisbn = "", OPTseries = "", OPTpages = "", OPTvolume = "" } @Misc{AL06OLD, OPTkey = {}, author = {R. Adams and Z. Luo}, title = {Formalisation of {Weyl's} predicative mathematics in type theory}, howpublished = {Talk at and manuscript submitted to {TYPES}'06}, OPTmonth = {}, year = {2006}, OPTnote = {}, OPTannote = {} } @Misc{AL06, OPTkey = {}, author = {R. Adams and Z. Luo}, title = {{Weyl's} predicative classical mathematics as a logic-enriched type theory}, howpublished = {Submitted to {TYPES}'06, to appear}, OPTmonth = {}, year = {2006}, OPTnote = {}, OPTannote = {} } @Article{luo:PALplus, author = {Z. Luo}, title = {{PAL}$^+$: a lambda-free logical framework}, journal = {Journal of Functional Programming}, year = {2003}, OPTkey = {}, volume = {13}, number = {2}, pages = {317-338}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{IsabelleHOL:02, author = {T. Nipkow and L. C. Paulson and M. Wenzel}, title = {Isabelle/{HOL}: a proof assistant for higher-order logic}, journal = {LNCS Tutorial 2283}, year = {2002}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Misc{luo:talk05, OPTcrossref = "", OPTkey = "", author = "Z. Luo", title = "A type-theoretic framework for mathematical pluralism", howpublished = "Talks given at TYPES'04 and several institutions", year = "2005", OPTmonth = "", OPTnote = "", OPTannote = "" } @Book{Issacs:68, author = "G. L. Issacs", title = "Real Numbers: a development of the real numbers in an axiomatic set theory", publisher = "McGraw Hill", year = "1968", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Misc{Agda:web, OPTcrossref = "", OPTkey = "", OPTauthor = "", title = "Agda proof assistant", howpublished = "\verb?http://www.cs.chalmers.se/~catarina/agda?", year = "2000", OPTmonth = "", OPTnote = "", OPTannote = "" } @Misc{Agda:web08, OPTcrossref = "", key = "Agda 2008", OPTauthor = "", title = "{Agda} proof assistant", howpublished = "\verb?http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?", year = "2008", OPTmonth = "", OPTnote = "", OPTannote = "" } @Book{Simpson:rev-math, author = "S. Simpson", title = "Subsystems of Second-Order Arithmetic", publisher = "Springer-Verlag", year = "1999", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @PHDTHESIS(Robin:thesis, AUTHOR = "R. Adams", TITLE = "A Modular Hierarchy of Logical Frameworks", SCHOOL = "University of Manchester", YEAR = "2004", MONTH = "", ADDRESS = "", NOTE = "", REVIEW = "" ) @Manual{Coq:manualv8, title = {The Coq Proof Assistant Reference Manual (Version 8.0), {INRIA}}, key = {Coq}, OPTauthor = {}, organization = {The Coq Development Team}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, year = {2004}, OPTnote = {}, OPTannote = {} } @Manual{Coq:manualv8.1, title = {The {Coq Proof Assistant Reference Manual (Version 8.1)}, {INRIA}}, key = {Coq 2007}, OPTauthor = {Coq}, organization = {The Coq Development Team}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, year = {2007}, OPTnote = {}, OPTannote = {} } @Article{Isabelle:94, author = {L. Paulson}, title = {Isabelle: a generic theorem prover}, journal = {LNCS}, year = {1994}, OPTkey = {}, volume = {828}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{Inductive:paulson98, author = {L. Paulson}, title = {The inductive approach to verifying cryptographic protocols}, journal = {Journal of Computer Security}, year = {1998}, OPTkey = {}, volume = {6}, OPTnumber = {}, pages = {85-128}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{ELF:93, author = "R. Harper and F. Honsell and G. Plotkin", title = "A Framework for Defining Logics", journal = "Journal of the Association for Computing Machinery", year = "1993", volume = "40", number = "1", pages = "143-184", OPTmonth = "", OPTnote = "" } @Article{BAN:89, author = "M. Burrows and M. Abadi and R. Needham", title = "A logic of authentication", journal = "Proc. of the Royal Society of London", year = "1989", volume = "426", OPTnumber = "", pages = "233-271", OPTmonth = "", OPTnote = "" } @Article{Paulson:LICS99, author = "L. Paulson", title = "Proving security protocols correct", journal = "{LICS}", year = "1999", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTmonth = "", OPTnote = "" } @Article{NS:78, author = "R. Needham and M. Schroeder", title = "Using encryption for authentication in large networks of computers", journal = "Comm. of the ACM", year = "1978", volume = "21", number = "12", pages = "993-999", OPTmonth = "", OPTnote = "" } @Article{Lowe:breakingNS96, author = "G. Lowe", title = "Breaking and fixing the {Needham-Schroeder} public-key protocol using {CSP} and {FDR}", journal = LNCS, year = "1996", volume = "1055", number = "", OPTpages = "147-166", OPTmonth = "", OPTnote = "" } @Article{Feferman:Weyl97, author = {S. Feferman}, title = {The significance of {Hermann Weyl's Das Kontinuum}}, year = {2000}, OPTkey = {}, volume = {Proof Theory, (eds) V. Hendricks et al.}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @InProceedings{robert-luo:TYPES03, author = "R. Kie{\ss}ling and Z. Luo", title = "Coercions in {Hindley-Milner} systems", booktitle = "Types for Proofs and Programs, Proc. of Inter. Conf. of {TYPES}'03, LNCS'3085.", year = "2004", OPTeditor = "", OPTpublisher = "", OPTisbn = "", OPTseries = "", OPTpages = "", OPTvolume = "" } @InProceedings{wadler:monads.functional, author = "P. Wadler", title = "Monads for functional programming", booktitle = "Advanced Functional Programming, LNCS'925", editor = "J. Jeuring and E. Meijer", year = "1995", pages = "24--52" } @InProceedings{mitchell83, author = "J. C. Mitchell", title = "Coercion and type inference", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTpages = "", booktitle = "{POPL}'83", year = "1983", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" @PhDThesis{damas:thesis, author = "L. Damas", title = "Type Assignment in Programming Languages", school = "University of Edinburgh", year = "1985", OPTnote = "CST-33-85" } @InProceedings{damas.milner:principal, author = "L. Damas and R. Milner", title = "Principal Type-Schemes for Functional Programs", booktitle = "Proc. of the 9th Ann. Symp. on Principles of Programming Languages", pages = "207-212", year = "1982" } @Article{milner:ML78, author = "R. Milner", title = "A theory of type polymorphism in programming", journal = "J. of Computer Systems and Sciences", year = "1978", volume = "17", OPTnumber = "", pages = "348-375", OPTmonth = "", OPTnote = "" } @TechReport{leroy:thesis, author = "X. Leroy", title = "Polymorphic typing of an algorithmic language", institution = "{INRIA}, Rocquencourt", year = "1992", type = "Tech Report", number = "RR-1778", OPTaddress = "", OPTmonth = "", note = "(English version of his PhD thesis at University of Paris 7.)" } @Article{leroy:manifest94, author = "X. Leroy", title = "Manifest types, modules and separate compilation", journal = "{POPL}'94", OPTpages = "207-212", year = "1994" } @Article{robinson:alg, author = "J. A. Robinson", title = "A machine-oriented logic based on the resolution principle", journal = "JACM", year = "1965", volume = "12", number = "1", pages = "23-41", OPTmonth = "", OPTnote = "" } @BOOK(Haskell:book03, AUTHOR = "S. Peyton-Jones", EDITOR = "", TITLE = "Haskell 98 Language and Libraries: the Revised Report", PUBLISHER = "Cambridge University Press", YEAR = "2003", MONTH = "", EDITION = "", NOTE = "", REVIEW = "") @BOOK(ML:book90, AUTHOR = "R. Milner and M. Tofts and R. Harper", EDITOR = "", TITLE = "The Definition of Standard {ML}", PUBLISHER = "MIT Press", YEAR = "1990", MONTH = "", EDITION = "", NOTE = "", REVIEW = "") @BOOK(ML:book97, AUTHOR = "R. Milner and M. Tofts, R. Harper and D. MacQueen", TITLE = "The Definition of Standard {ML} (Revised)", PUBLISHER = "MIT", YEAR = "1997" ) @BOOK(CAML:book00, AUTHOR = "X. Leroy", EDITOR = "", TITLE = "The Objective Caml system: documentation and user's manual", PUBLISHER = "", YEAR = "2000", MONTH = "", EDITION = "", NOTE = "Available \verb?http://caml.inria.fr/?", REVIEW = "") @InProceedings{Clean, author = "T. Brus and M. van Eekelen and M. van Leer and M. Plasmeijer", title = "Clean: a language for functional graph rewriting", booktitle = "Functional Programming and Computer Architecture, {LNCS}'274", editor = "G. Kahn", pages = "364-384", year = "1987" } @InProceedings{jones.jones.meijer:typeclasses, author = "S. Peyton-Jones and M. Jones and E. Meijer", title = "Type Classes: An Exploration of the Design Space", booktitle = "Proceedings of the Haskell Workshop June 1997, Amsterdam", year = 1997 } @Article{hindley:principal, author = "R. Hindley", title = "The princial type-scheme of an object in combinatory logic", journal = "Trans. of the American Math Society", year = "1969", volume = "146", OPTnumber = "1", pages = "29-60", OPTmonth = "", OPTnote = "" } @Article{mitchell91, author = "J. C. Mitchell", title = "Type inference with simple subtypes", OPTcrossref = "", OPTkey = "", journal = "J of Func. Prog.", year = "1991", volume = "1", number = "2", OPTpages = "245-286", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{LL05, author = "Z. Luo and Y. Luo", title = "Transitivity in coercive subtyping", journal = "Infor.and Comput.", year = "2005", volume = "197", number = "1-2", OPTpages = "122-144", OPTmonth = "", OPTnote = "" } @PhdThesis{yong:thesis, author = {Y. Luo}, title = {Coherence and Transitivity in Coercive Subtyping}, school = {University of Durham}, year = {2005}, OPTkey = {}, OPTtype = {}, OPTaddress = {}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Article{cardelli.wegner:understanding, author = "L. Cardelli and P. Wegner", title = "On Understanding Types, Data Abstraction and Polymorphism", journal = "Computing Surveys", year = "1985", volume = "17", number = "4", signature = "GI/ZA-90", pages = "471--522" } @UNPUBLISHED(Pottier:ML05, AUTHOR = "F. Pottier", TITLE = "A modern eye on {ML} type inference", YEAR = "2005", MONTH = "", NOTE = "Lecture notes for the {APPSEM} Summer School", REVIEW = "" ) @Article{Strachey:67, author = "C. Strachey", title = "Fundamental Concepts in Programming Languages", journal = "Higher-Order and Symbolic Computation", year = "2000", volume = "13", number = "1-2", pages = "11-49" } @Manual{Coq-manual-v8.0, title = {The Coq Proof Assistant Reference Manual (Version 8.0), {INRIA}}, key = {Coq}, OPTauthor = {}, organization = {The Coq Development Team}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, year = {2004}, OPTnote = {}, OPTannote = {} } @Article{Odersky:99, author = "M. Odersky and M. Sulzmann and M. Wehr", title = "Type inference with constrained types", journal = "Theory and Practice of Object Systems", year = "1999", volume = "5", number = "1", OPTpages = "" } @Article{Pollack:records02, author = "R. Pollack", title = "Dependently typed records in type theory", journal = "Formal Aspects of Computing", year = "2002", volume = "13", number = "3-5", OPTpages = "386-402" } @Article{Harper-Lillibridge93, author = "R. Harper and M. Lillibridge", title = "A type-theoretic approach to higher-order modules with sharing", journal = "{POPL}'94", year = "1994", OPTvolume = "", OPTnumber = "", OPTpages = "123-137" } @Article{ctp:semantic-records05, author = "T. Coquand and R. Pollack and M. Takeyama", title = "A logical framework with dependently typed records", journal = "Fundamenta Informaticae", year = "2005", volume = "65", number = "1-2", OPTpages = "" } @InProceedings{coen-tassi08:TYPES07, author = "C. Sacerdoti-Coen and E. Tassi", title = "Working with mathematical structures in type theory", booktitle = "Types for Proofs and Programs, {LNCS}'4941", year = "2008", OPTeditor = "M. Miculan and I. Scagnetto and F. Honsell", OPTpublisher = "Springer-Verlag", OPTisbn = "3-540-68084-5", OPTseries = "LNCS", OPTpages = "157-172", OPTvolume = "4941" } @Book{OOP:book94, OPTauthor = "", title = "Theoretical Aspects of Object-Oriented Programming", publisher = "MIT", year = "1994", editor = "C. A. Gunter and J. C. Mitchell", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Book{abadi-cardelli:book96, author = "M. Abadi and L. Cardelli", title = "A Theory of Objects", publisher = "Springer", year = "1996", OPTeditor = "", OPTvolume = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "" } @Article{Kamin:self-app88, author = "S. Kamin", title = "Inheritance in {Smalltalk-80}: a denotational definition", journal = "{POPL}'88", OPTyear = "1988", OPTvolume = "", OPTnumber = "80-8", OPTpages = "" } @InProceedings{Kamin-Reddy:self-app94, author = "S. Kamin and U. Reddy", title = "\hspace{-.04in}{Two} semantic models of object-oriented languages\hspace{-.02in}", booktitle = "\hspace{-.02in}\cite{OOP:book94}", OPTyear = "\hspace{-.04in}1996", OPTeditor = "", OPTpublisher = "", OPTisbn = "", OPTseries = "", OPTpages = "463-495", OPTvolume = "" } @Article{cardelli:record88, author = "L. Cardelli", title = "A semantics of multiple inheritence", journal = "Infor. and Comp.", year = "1988", volume = "76", number = "2/3", OPTpages = "" } @InProceedings{constable-hickey:class00, author = "R. Constable and J. Hickey", title = "Nuprl's class theory and its applications", booktitle = "Foundations of Secure Computation", year = "2000", OPTeditor = "F. L. Bauer and R. Steinbruggen", publisher = "{IOS Press}, Amsterdam", OPTisbn = "", OPTseries = "", OPTpages = "91-115", OPTvolume = "" } @Article{pierce-turner:state-app94, author = "B. C. Pierce and D. N. Turner", title = "Simple type-theoretic foundations for object-oriented programming", journal = "J. of Functional Programming", year = "1994", volume = "4", number = "2", pages = "207-247" } @article{pierce:virtual99, author = "A. Igarashi and B. C. Pierce", title = "Foundations for Virtual Types", journal = "{LNCS}'1628", OPTvolume = "1628", OPTpages = "", year = "1999", OPTurl = "citeseer.ist.psu.edu/247207.html" } @BOOK(KeY:book07, OPTAUTHOR = "", EDITOR = "B. Beckert and R. Hahnle and P. H. Schmitt", TITLE = "Verification of Object-Oriented Software: the {KeY} Approach, {LNCS}'4334", PUBLISHER = "Springer", YEAR = "2007", MONTH = "", EDITION = "", NOTE = "", REVIEW = "") @article{Krakatoa:04, author = "C. Marche and C. Paulin-Mohring and X. Urbain", title = "The {KRAKATOA} tool for certification of {JAVA/JAVACARD} programs annotated in {JML}", journal = "Journal of Logic and Algebraic Programming", volume = "58", number = "1-2", pages = "89-106", year = "2004" } @article{ESC-Java:TLDI02, author = "C. Flanagan and others", title = "Extended Static Checking for {Java}", journal = "{PLDI}'02", OPTvolume = "", OPTnumber = "", OPTpages = "", year = "2002" } @article{LOOP:01, author = "J. van den Berg and B. Jacobs", title = "The {LOOP} compiler for {Java} and {JML}", journal = "{LNCS}'2031", OPTvolume = "", OPTnumber = "", OPTpages = "", OPTyear = "2001" } @InProceedings{Spec:04, author = "M. Barnett and K. R. M. Leino, and W. Schulte", title = "The {Spec\#} programming system: an overview", booktitle = "{CASSIS} 2004, LNCS'3362", year = "2004", OPTeditor = "", OPTpublisher = "Springer-Verlag", OPTisbn = "", OPTseries = "Lecture Notes in Computer Science", OPTpages = "", OPTvolume = "3362" } @article{abadi-cardelli:PER94, author = "M. Abadi and L. Cardelli", title = "A semantics of object types", journal = "{LICS}'94", OPTvolume = "", OPTnumber = "", OPTpages = "", year = "1994" } @article{luo:poly08, author = "Z. Luo", title = "Coercions in a polymorphic type system", journal = "Mathematical Structures in Computer Science", volume = "18", number = "4", OPTpages = "", year = "2008", OPTNOTE = "(In press)" } @article{luo-adams:MSCS08, author = "Z. Luo and R. Adams", title = "Structural subtyping for inductive types with functorial equality rules", journal = "Mathematical Structures in Computer Science", volume = "18", number = "5", OPTpages = "", year = "2008", OPTNOTE = "(In press)" } @Misc{Matita:web08, OPTcrossref = "", key = "Matita 2008", OPTauthor = "", title = "The {Matita} proof assistant", howpublished = "\verb?http://matita.cs.unibo.it/?", year = "2008", OPTmonth = "", OPTnote = "", OPTannote = "" } @article{Nuprl:innovations06, author = "S. Allen and others", title = "Innovations in computational type theory using {Nuprl}", journal = "Journal of Applied Logic", volume = "4", number = "4", OPTpages = "", year = "2006" } @article{luo:Module08manuscript, author = "Z. Luo", title = "Module mechanisms in intensional type theory", journal = "Manuscript", OPTvolume = "", OPTnumber = "", OPTpages = "", year = "2008" } @Manual{Coq:manualv8.1TYPES08, title = {The {Coq Proof Assistant Reference Manual (Version 8.1)}, {INRIA}}, key = {Coq 2007}, OPTauthor = {Coq}, organization = {The Coq Development Team}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, year = {2007}, OPTnote = {}, OPTannote = {} } @Misc{Agda:webTYPES08, OPTcrossref = "", key = "Agda 2008", OPTauthor = "", title = "The {Agda} proof assistant (Version 2)", howpublished = "Available from the web page: \verb?http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?", year = "2008", OPTmonth = "", OPTnote = "", OPTannote = "" } @Misc{luo:ESOP09draft, OPTcrossref = "", OPTkey = "", author = "Z. Luo", title = "Intensional manifest fields with application to modelling object-oriented features", howpublished = "Draft paper", year = "2008", OPTmonth = "July", OPTnote = "", OPTannote = "" } @article{stone-harper:TOCL06, author = "C. Stone and R. Harper", title = "Extensional equivalence and singleton types", journal = "{ACM} Trans. on Computational Logic", volume = "7", number = "4", pages = "676 - 722", year = "2006" } @InProceedings{luo:TYPES08, author = "Z. Luo", title = "Manifest fields and module mechanisms in intensional type theory", booktitle = "{LNCS} 5497", year = "2009", OPTeditor = "S. Berardi and F. Damiani and U. de'Liguoro", OPTpublisher = "", OPTisbn = "", OPTseries = "", OPTpages = "", OPTvolume = "" } @article{luo:TYPES08short, author = "Z. Luo", title = "Manifest fields and module mechanisms in intensional type theory", journal = "Types for Proofs and Programs ({TYPES}'08), {LNCS} 5497.", year = "2009", OPTeditor = "S. Berardi and F. Damiani and U. de'Liguoro", OPTpublisher = "", OPTisbn = "", OPTseries = "", OPTpages = "", OPTvolume = "" } @article{luo:MLPA09subm, author = "Z. Luo", title = "Dependent Record Types Revisited", journal = "Modules and Libraries for Proof Assistants (MLPA'09) ", year = "2009", OPTeditor = "", OPTpublisher = "", OPTisbn = "", OPTseries = "", OPTpages = "", OPTvolume = "", note = "To appear" } @article{luo:MLPA09, author = "Z. Luo", title = "Dependent Record Types Revisited", journal = "Proc. of the 1st Inter. Workshop on Modules and Libraries for Proof Assistants (MLPA'09), Montreal. ", year = "2009", OPTeditor = "", OPTpublisher = "", OPTisbn = "", OPTseries = "", OPTpages = "", volume = "ACM Inter. Conf. Proceeding Series, Vol 429", OPTnote = "" } @Misc{luo:linguistics09, OPTcrossref = "", OPTkey = "", author = "Z. Luo", title = "Type theory and coercive subtyping in linguistic semantics", howpublished = "Draft", year = "2009", OPTmonth = "", OPTnote = "", OPTannote = "" } @article{Asher:dot08, author = "N. Asher", title = "A type driven theory of predication with complex types", journal = "Fundamenta Infor.", volume = "84", number = "2", OPTpages = "151-183", year = "2008" } @InProceedings{Montague:PTQ73, author = "R. Montague", title = "The proper treatment of quantification in ordinary {English}", booktitle = "Approaches to Natural Languages", year = "1973", editor = "J. Hintikka and J. Moravcsik and P. Suppes", OPTpublisher = "", OPTisbn = "", OPTseries = "", OPTpages = "", OPTvolume = "" } @BOOK(Barwise:situation83, AUTHOR = "J. Barwise and J. Perry", OPTEDITOR = "", TITLE = "Situations and Attitudes", PUBLISHER = "MIT Press", YEAR = "1983", MONTH = "", EDITION = "", NOTE = "", REVIEW = "") @BOOK(montague:74, AUTHOR = "R. Montague", OPTEDITOR = "", TITLE = "Formal Philosophy", PUBLISHER = "Yale University Press", YEAR = "1974", OPTMONTH = "", OPTEDITION = "", NOTE = "(Collection edited by R. Thomason)", OPTREVIEW = "") @BOOK(DRT:93, AUTHOR = "H. Kamp and U. Reyle", OPTEDITOR = "", TITLE = "From Discourse to Logic", PUBLISHER = "Kluwer", YEAR = "1993", OPTMONTH = "", OPTEDITION = "", OPTNOTE = "", OPTREVIEW = "") @article{LA:functorial08, author = "Z. Luo and R. Adams", title = "Structural subtyping for inductive types with functorial equality rules.", journal = "Mathematical Structures in Computer Science", volume = "18", number = "5", pages = "931-972", year = "2008" } @Misc{Pus:05survey, OPTcrossref = "", OPTkey = "", author = "J. Pustejovsky", title = "A survey of dot objects", howpublished = "Manuscript", year = "2005", OPTmonth = "", OPTnote = "", OPTannote = "" } @Misc{luo:notes09-06-05, OPTcrossref = "", OPTkey = "", author = "Z. Luo", title = "Type-Theoretical Semantics with Coercive Subtyping", howpublished = "Notes", year = "2009", OPTmonth = "", OPTnote = "", OPTannote = "" } @Misc{AsherPustejovsky:05, OPTcrossref = "", OPTkey = "", author = "N. Asher and J. Pustejovsky", title = "Word meaning and commonsense metaphysics", OPThowpublished = "", year = "2005", OPTmonth = "", OPTnote = "", OPTannote = "" } @BOOK(asher:book09draft, AUTHOR = "N. Asher", OPTEDITOR = "", TITLE = "{Lexical Meaning in Context: A Web of Words}", OPTPUBLISHER = "", YEAR = "2009", OPTMONTH = "June", OPTEDITION = "", NOTE = "(Draft book to be published by CUP)", OPTREVIEW = "") @article{gonthier:4colour08, author = "G. Gonthier", title = "Formal Proof--The Four-Color Theorem", journal = "Notices of the American Math. Society", volume = "55", number = "11", OPTpages = "", year = "2008" } @article{cooper:dot07, author = "R. Cooper", title = "Copredication, dynamic generalized quantification and lexical innovation by coercion", journal = "Proceedings of GL2007, the Fourth International Workshop on Generative Approaches to the Lexicon", OPTvolume = "", OPTnumber = "", OPTpages = "", year = "2007" } @article{cooper:record05, author = "R. Cooper", title = "Records and record types in semantic theory", journal = "J of Logic and Computation", volume = "15", number = "2", OPTpages = "", year = "2005" } @InProceedings{marlet:GL07, author = "R. Marlet", title = "When the generative lexicon meets computational semantics", booktitle = "{Proc of the 4th Inter. Workshop on Generative Approaches to the Lexicon (GL 2007)}", year = "2007", OPTeditor = "", OPTpublisher = "", OPTisbn = "", OPTseries = "", OPTpages = "", OPTvolume = "" } @article{thorsten-conor-wouter:OTT07, author = "T. Altenkirch and C. McBride and W. Swierstra", title = "{Observational Equality, Now!}", journal = "{Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification (PLPV 2007)}", OPTvolume = "", OPTnumber = "", OPTpages = "", year = "2007" } @article{retore:09, author = "C. Bassac and B. Mery and C. Retor\'{e}", title = "{Towards a Type-theoretical account of lexical semantics}", journal = "{J of Logic, Language and Information}", volume = "19", number = "2", OPTpages = "", year = "2009" }