adam@310: @Book{TAPL, adam@310: author = "Benjamin C. Pierce", adam@310: title = "Types and Programming Languages", adam@310: year = "2002", adam@310: publisher = "MIT Press" adam@310: } adam@310: adam@310: @Book{CAR, adam@310: author = "Matt Kaufmann and Panagiotis Manolios and J Strother Moore", adam@310: title = "Computer-Aided Reasoning: An Approach", adam@310: year = "2000", adam@310: publisher = "Kluwer Academic Publishers" adam@310: } adam@310: adam@310: @Article{AMD, adam@310: author = {J Strother Moore and Tom Lynch and Matt Kaufmann}, adam@310: title = {A Mechanically Checked Proof of the Correctness of the Kernel of the {AMD5k86} Floating-Point Division Algorithm}, adam@310: journal = {IEEE Transactions on Computers}, adam@310: volume = {47(9)}, adam@310: pages = {913--926} adam@310: year = {1998} adam@310: } adam@310: adam@310: @Book{Piton, adam@310: author={J Strother Moore}, adam@310: title = {Piton: A Mechanically Verified Assembly-Level Language}, adam@310: year = "1996", adam@310: series = "Automated Reasoning Series", adam@310: publisher = "Kluwer Academic Publishers" adam@310: } adam@310: adam@310: @Article{Nqthm, adam@310: title = {The {Boyer-Moore} Theorem Prover and Its Interactive Enhancement}, adam@310: author = {Robert S. Boyer and Matt Kaufmann and J Strother Moore}, adam@310: journal = {Computers and Mathematics with Applications}, adam@310: volume = {29(2)}, adam@310: year = {1995}, adam@310: pages = {27--62} adam@310: } adam@310: adam@310: @Article{4C, adam@310: author = {Gonthier, Georges}, adam@310: year = {2008}, adam@310: title = {Formal Proof--The Four-Color Theorem}, adam@310: journal = {Notices of the American Mathematical Society}, adam@310: volume = {55(11)}, adam@310: pages = {1382-–1393} adam@310: } adam@310: adam@310: @Article{CompCert, adam@310: author = {Leroy, Xavier}, adam@310: year = {2009}, adam@310: title = {A formally verified compiler back-end}, adam@310: journal = {Journal of Automated Reasoning}, adam@310: volume = {43(4)}, adam@310: pages = {363--446} adam@310: } adam@310: adam@310: @InProceedings{seL4, adam@310: author = {Gerwin Klein adam@310: and Kevin Elphinstone adam@310: and Gernot Heiser adam@310: and June Andronick adam@310: and David Cock adam@310: and Philip Derrin adam@310: and Dhammika Elkaduwe adam@310: and Kai Engelhardt adam@310: and Rafal Kolanski adam@310: and Michael Norrish adam@310: and Thomas Sewell adam@310: and Harvey Tuch adam@310: and Simon Winwood}, adam@310: title = {{seL4}: Formal Verification of an {OS} Kernel}, adam@310: booktitle = {Proceedings of the 22nd {ACM Symposium on Operating Systems Principles}}, adam@310: year = {2009}, adam@310: } adam@310: adam@310: @Book{Isabelle/HOL, adam@310: author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, adam@310: title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic}, adam@310: publisher = {Springer}, adam@310: series = {Lecture Notes in Computer Science}, adam@310: volume = 2283, adam@310: year = 2002 adam@310: } adam@310: adam@310: @Book{Isabelle, adam@310: author = {Paulson, Lawrence C.}, adam@310: year = {1994}, adam@310: title = {Isabelle: A Generic Theorem Prover}, adam@310: series = {Lecture Notes in Computer Science}, adam@310: volume = {828}, adam@310: publisher = {Springer} adam@310: } adam@310: adam@310: @Book{CoqArt, adam@310: author = "Bertot, Yves and Cast\'eran, Pierre", adam@310: title = "Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions", adam@310: series = "Texts in Theoretical Computer Science", adam@310: year = "2004", adam@310: publisher = "Springer Verlag", adam@310: } adam@310: adam@310: @unpublished{CoqManual, adam@310: author = "{Coq Development Team}", adam@310: title = "The {Coq} proof assistant reference manual, version 8.3", adam@310: year = 2010, adam@310: url={http://coq.inria.fr/refman/} adam@310: } adam@311: adam@311: @inproceedings{CIC, adam@311: author = {Christine Paulin-Mohring}, adam@311: title = {Inductive Definitions in the System {Coq} - Rules and Properties}, adam@311: year = {1993}, adam@311: booktitle = {Proceedings of the International Conference on {Typed Lambda Calculi and Applications}}, adam@311: } adam@311: adam@311: @inproceedings{SetsInTypes, adam@311: author = {Benjamin Werner}, adam@311: title = {Sets in Types, Types in Sets}, adam@311: booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software}, adam@311: year = {1997}, adam@311: } adam@311: adam@311: @article{CoC, adam@311: author = {Thierry Coquand and G\'erard Huet}, adam@311: title = {The {Calculus} of {Constructions}}, adam@311: journal = {Information and Computation}, adam@311: volume = {76(2-3)}, adam@311: year = {1988} adam@311: } adam@312: adam@315: @inproceedings{GADT, adam@312: author = {Hongwei Xi and Chiyan Chen and Gang Chen}, adam@312: title = {Guarded Recursive Datatype Constructors}, adam@312: booktitle = {Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages}, adam@312: year = {2003} adam@312: } adam@315: adam@315: @article{Curry, adam@315: title={Functionality in Combinatory Logic}, adam@315: author = {H. B. Curry}, adam@315: journal = {Proceedings of the National Academy of Sciences of the United States of America}, adam@315: volume = {20(11)}, adam@315: year = {1934}, adam@315: pages = {584--590} adam@315: } adam@315: adam@315: @incollection{Howard, adam@315: author = {Howard, William A.}, adam@315: title = {The formulae-as-types notion of construction}, adam@315: editor = {Seldin, Jonathan P. and Hindley, J. Roger}, adam@315: booktitle = {To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism}, adam@315: publisher = {Academic Press}, adam@315: pages = {479--490}, adam@315: year = {1980}, adam@315: note = {Original paper manuscript from 1969} adam@315: } adam@316: adam@316: @inproceedings{HOAS, adam@316: author = {Pfenning, F. and Elliot, C.}, adam@316: title = {Higher-order abstract syntax}, adam@316: booktitle = {Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation}, adam@316: year = {1988}, adam@316: pages = {199--208}, adam@316: } adam@317: adam@317: @article{HOU, adam@317: author = {G\'erard Huet}, adam@317: title = {The undecidability of unification in third order logic}, adam@317: journal = {Information and Control}, adam@317: voluem = {22(3)}, adam@317: year = {1973}, adam@317: pages = {257--267} adam@317: } adam@328: adam@328: @InBook{TAPLNatDed, adam@328: author = "Benjamin C. Pierce", adam@328: title = "Types and Programming Languages", adam@328: year = "2002", adam@328: publisher = "MIT Press", adam@328: chapter = "9.4" adam@328: } adam@328: adam@328: @inproceedings{Monads, adam@328: author = {Wadler, Philip}, adam@328: title = {The essence of functional programming}, adam@328: booktitle = {Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, adam@328: year = {1992}, adam@328: } adam@328: adam@328: @inproceedings{IO, adam@328: author = {Peyton Jones, Simon L. and Wadler, Philip}, adam@328: title = {Imperative functional programming}, adam@328: booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, adam@328: year = {1993}, adam@328: } adam@328: adam@328: @InProceedings{separation, adam@328: author = {John C. Reynolds}, adam@328: title = {Separation Logic: A Logic for Shared Mutable Data Structures}, adam@328: booktitle = {Proceedings of the IEEE Symposium on Logic in Computer Science}, adam@328: year = {2002} adam@338: } adam@338: adam@338: @article{Okasaki, adam@338: author = {Okasaki, Chris}, adam@338: title = {Red-black trees in a functional setting}, adam@338: journal = {J. Funct. Program.}, adam@338: volume = {9}, adam@338: issue = {4}, adam@338: year = {1999}, adam@338: pages = {471--477}, adam@338: } adam@342: adam@342: @Article{DeBruijn, adam@342: author = "Nicolas G. de Bruijn", adam@342: title = "Lambda-calculus notation with nameless dummies: a tool for automatic formal manipulation with application to the {Church-Rosser} theorem", adam@342: journal = "Indag. Math.", adam@342: volume = "34(5)", adam@342: pages = "381--392", adam@342: year = "1972" adam@342: } adam@343: adam@343: @INPROCEEDINGS{GirardsParadox, adam@343: author = {Thierry Coquand}, adam@343: title = {An Analysis of {Girard's} Paradox}, adam@343: booktitle = {Proceedings of the Symposium on Logic in Computer Science}, adam@343: year = {1986}, adam@343: pages = {227--236} adam@343: } adam@344: adam@344: @inproceedings{PCC, adam@344: author = {George C. Necula}, adam@344: title = {Proof-carrying code}, adam@344: booktitle = {Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, adam@344: year = {1997}, adam@344: } adam@344: adam@344: @inproceedings{XCAP, adam@344: author = {Ni, Zhaozhong and Shao, Zhong}, adam@344: title = {Certified assembly programming with embedded code pointers}, adam@344: booktitle = {Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, adam@344: year = {2006}, adam@344: } adam@346: adam@346: @TechReport{IT, adam@346: title = "A Tutorial on Recursive Types in {Coq}", adam@346: author = "Eduardo Gim\'enez", adam@346: year = "1998", adam@346: month = may, adam@346: number = "0221", adam@346: institution = "INRIA", adam@346: } adam@347: adam@347: @inproceedings{BigStep, adam@347: author = {Xavier Leroy and Herv\'e Grall}, adam@347: title = {Coinductive big-step operational semantics}, adam@347: year = {2006}, adam@347: booktitle = {Proceedings of the 15th European Symposium on Programming} adam@347: } adam@355: adam@355: @InBook{WinskelDomains, adam@355: author = "Glynn Winskel", adam@355: title = "The Formal Semantics of Programming Languages", adam@355: year = "1993", adam@355: publisher = "MIT Press", adam@355: chapter = "8" adam@355: } adam@356: adam@356: @article{Capretta, adam@356: author = {Venanzio Capretta}, adam@356: title = {General Recursion via Coinductive Types}, adam@356: journal = {Logical Methods in Computer Science}, adam@356: volume = 1, adam@356: number = 2, adam@356: year = 2005, adam@356: pages = {1--18}, adam@356: } adam@356: adam@356: @inproceedings{Megacz, adam@356: author = {Adam Megacz}, adam@356: title = {A coinductive monad for prop-bounded recursion}, adam@356: booktitle = {Proceedings of the {ACM} Workshop Programming adam@356: Languages meets Program Verification}, adam@356: pages = {11--20}, adam@356: year = {2007}, adam@356: } adam@358: adam@358: @inproceedings{modules, adam@358: author = {MacQueen, David}, adam@358: title = {Modules for {Standard ML}}, adam@358: booktitle = {Proceedings of the 1984 ACM Symposium on LISP and Functional Programming}, adam@358: year = {1984}, adam@358: pages = {198--207}, adam@358: } adam@358: adam@358: @inproceedings{typeclasses, adam@358: author = {Wadler, P. and Blott, S.}, adam@358: title = {How to make ad-hoc polymorphism less ad hoc}, adam@358: booktitle = {Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, adam@358: year = {1989}, adam@358: pages = {60--76}, adam@358: } adam@360: adam@360: @inproceedings{reflection, adam@360: author = {Boutin, Samuel}, adam@360: title = {Using reflection to build efficient and certified decision procedures}, adam@360: booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software}, adam@360: year = {1997}, adam@360: } adam@364: adam@364: @inproceedings{JMeq, adam@364: author = {McBride, Conor}, adam@364: title = {Elimination with a Motive}, adam@364: booktitle = {Proceedings of the International Workshop on Types for Proofs and Programs}, adam@364: year = {2000}, adam@364: pages = {197--216} adam@364: } adam@364: adam@364: @phdthesis{AxiomK, adam@364: author = {Thomas Streicher}, adam@364: title = {Semantical Investigations into Intensional Type Theory}, adam@364: type = {Habilitationsschrift}, adam@364: school = {LMU M\"unchen}, adam@364: year= {1993} adam@364: } adam@381: adam@381: @article{BGB, adam@381: author = {Geoffrey Washburn and Stephanie Weirich}, adam@381: title = {Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism}, adam@381: journal = {J. Funct. Program.}, adam@381: volume = {18}, adam@381: number = {1}, adam@381: year = {2008}, adam@381: pages = {87--140}, adam@381: publisher = {Cambridge University Press}, adam@381: address = {New York, NY, USA}, adam@381: } adam@381: adam@381: @InProceedings{PhoasICFP08, adam@381: author = {Adam Chlipala}, adam@381: title = {Parametric Higher-Order Abstract Syntax for Mechanized Semantics}, adam@381: booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming}, adam@381: year = {2008}, adam@381: pages = {143--156} adam@381: } adam@381: adam@381: @article{parametricity, adam@381: author = {Reynolds, J.C.}, adam@381: year = {1983}, adam@381: title = {Types, abstraction, and parametric polymorphism}, adam@381: journal = {Information Processing}, adam@381: pages = {513--523} adam@381: } adam@381: adam@381: @InProceedings{CompilerPOPL10, adam@381: author = {Adam Chlipala}, adam@381: title = {A Verified Compiler for an Impure Functional Language}, adam@381: booktitle = {Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, adam@381: year = {2010}, adam@381: } adam@387: adam@387: @inproceedings{Isar, adam@387: author = {Wenzel, Markus}, adam@387: title = {Isar - A Generic Interpretative Approach to Readable Formal Proof Documents}, adam@387: booktitle = {Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics}, adam@387: series = {TPHOLs '99}, adam@387: year = {1999}, adam@387: isbn = {3-540-66463-7}, adam@387: pages = {167--184}, adam@387: numpages = {18}, adam@387: url = {http://dl.acm.org/citation.cfm?id=646526.694887}, adam@387: acmid = {694887}, adam@387: publisher = {Springer-Verlag}, adam@387: address = {London, UK, UK}, adam@387: }