286 lines
No EOL
8.6 KiB
BibTeX
286 lines
No EOL
8.6 KiB
BibTeX
@inproceedings{Allais-et-al-2017,
|
|
title={Type-and-scope safe programs and their proofs},
|
|
author={Allais, Guillaume and Chapman, James and McBride, Conor and McKinna, James},
|
|
booktitle={Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs},
|
|
pages={195--207},
|
|
year={2017},
|
|
organization={ACM}
|
|
}
|
|
|
|
@inproceedings{Altenkirch-and-Reus-1999,
|
|
title={Monadic presentations of lambda terms using generalized inductive types},
|
|
author={Altenkirch, Thorsten and Reus, Bernhard},
|
|
booktitle={International Workshop on Computer Science Logic},
|
|
pages={453--468},
|
|
year={1999},
|
|
organization={Springer}
|
|
}
|
|
|
|
@article{Avigad-and-Harrison-2014,
|
|
title={Formally verified mathematics},
|
|
author={Avigad, Jeremy and Harrison, John},
|
|
journal={Communications of the ACM},
|
|
volume={57},
|
|
number={4},
|
|
pages={66--75},
|
|
year={2014},
|
|
publisher={ACM}
|
|
}
|
|
|
|
@inproceedings{Berger-1993,
|
|
title={Program extraction from normalization proofs},
|
|
author={Berger, Ulrich},
|
|
booktitle={International Conference on Typed Lambda Calculi and Applications},
|
|
pages={91--106},
|
|
year={1993},
|
|
organization={Springer}
|
|
}
|
|
|
|
@inproceedings{Bove-and-Capretta-2001,
|
|
title={Nested general recursion and partiality in type theory},
|
|
author={Bove, Ana and Capretta, Venanzio},
|
|
booktitle={International Conference on Theorem Proving in Higher Order Logics},
|
|
pages={121--125},
|
|
year={2001},
|
|
organization={Springer}
|
|
}
|
|
|
|
@inproceedings{Bove-et-al-2009,
|
|
title={A brief overview of Agda--a functional language with dependent types},
|
|
author={Bove, Ana and Dybjer, Peter and Norell, Ulf},
|
|
booktitle={International Conference on Theorem Proving in Higher Order Logics},
|
|
pages={73--78},
|
|
year={2009},
|
|
organization={Springer}
|
|
}
|
|
|
|
@article{Capretta-2005,
|
|
title={General recursion via coinductive types},
|
|
author={Venanzio Capretta},
|
|
journal={Logical Methods in Computer Science},
|
|
volume={1},
|
|
number={2},
|
|
year={2005}
|
|
}
|
|
|
|
@phdthesis{Chapman-2009,
|
|
title={Type checking and normalisation},
|
|
author={Chapman, James Maitland},
|
|
year={2009},
|
|
school={University of Nottingham}
|
|
}
|
|
|
|
@inproceedings{Danas-et-al-2017,
|
|
title={User Studies of Principled Model Finder Output},
|
|
author={Danas, Natasha and Nelson, Tim and Harrison, Lane and Krishnamurthi, Shriram and Dougherty, Daniel J},
|
|
booktitle={International Conference on Software Engineering and Formal Methods},
|
|
pages={168--184},
|
|
year={2017},
|
|
organization={Springer}
|
|
}
|
|
|
|
@inproceedings{Dagand-and-Scherer-2015,
|
|
title={Normalization by realizability also evaluates},
|
|
author={Dagand, Pierre-{\'E}variste and Scherer, Gabriel},
|
|
booktitle={Vingt-sixi{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs (JFLA 2015)},
|
|
year={2015}
|
|
}
|
|
|
|
@book {Felleisen-et-al-2009,
|
|
title = {Semantics engineering with PLT Redex},
|
|
author = {Felleisen, Matthias and Findler, Robert Bruce and Flatt, Matthew},
|
|
year = {2009},
|
|
publisher = {By Press}
|
|
}
|
|
|
|
@techreport{Goguen-and-McKinna-1997,
|
|
title={Candidates for substitution},
|
|
author={Goguen, Healfdene and McKinna, James},
|
|
institution={Laboratory for Foundations of Computer Science, University of Edinburgh},
|
|
year={1997}
|
|
}
|
|
|
|
@incollection{Gonthier-2008,
|
|
title={The four colour theorem: Engineering of a formal proof},
|
|
author={Gonthier, Georges},
|
|
booktitle={Computer mathematics},
|
|
pages={333--333},
|
|
year={2008},
|
|
publisher={Springer}
|
|
}
|
|
|
|
@inproceedings{Gonthier-et-al-2013,
|
|
title={A machine-checked proof of the odd order theorem},
|
|
author={Gonthier, Georges and Asperti, Andrea and Avigad, Jeremy and others},
|
|
booktitle={International Conference on Interactive Theorem Proving},
|
|
pages={163--179},
|
|
year={2013},
|
|
organization={Springer}
|
|
}
|
|
|
|
@inproceedings{Hales-et-al-2017,
|
|
title={A formal proof of the {K}epler conjecture},
|
|
author={Hales, Thomas and Adams, Mark and Bauer, Gertrud and Dang, Tat Dat and Harrison, John and Le Truong, Hoang and Kaliszyk, Cezary and Magron, Victor and McLaughlin, Sean and Nguyen, Tat Thang and others},
|
|
booktitle={Forum of Mathematics, Pi},
|
|
volume={5},
|
|
year={2017},
|
|
organization={Cambridge University Press}
|
|
}
|
|
|
|
@book{Harper-2016,
|
|
title={Practical foundations for programming languages},
|
|
author={Harper, Robert},
|
|
year={2016},
|
|
publisher={Cambridge University Press}
|
|
}
|
|
|
|
@article{Huet-et-al-1997,
|
|
title={The {C}oq proof assistant a tutorial},
|
|
author={Huet, G{\'e}rard and Kahn, Gilles and Paulin-Mohring, Christine},
|
|
journal={Rapport Technique},
|
|
volume={178},
|
|
year={1997}
|
|
}
|
|
|
|
@inproceedings{Kastner-et-al-2017,
|
|
title={Closing the gap--the formally verified optimizing compiler CompCert},
|
|
author={K{\"a}stner, Daniel and Leroy, Xavier and Blazy, Sandrine and Schommer, Bernhard and Schmidt, Michael and Ferdinand, Christian},
|
|
booktitle={SSS'17: Safety-critical Systems Symposium 2017},
|
|
pages={163--180},
|
|
year={2017},
|
|
organization={CreateSpace}
|
|
}
|
|
|
|
@misc{Kiselyov-2009,
|
|
author={Oleg Kiselyov},
|
|
title={Formalizing languages, mechanizing type-soundess and other meta-theoretic proofs},
|
|
note={unpublished manuscript},
|
|
url={http://okmij.org/ftp/formalizations/index.html},
|
|
year={2009}
|
|
}
|
|
|
|
@inproceedings{Klein-2009,
|
|
title={seL4: Formal verification of an OS kernel},
|
|
author={Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and others},
|
|
booktitle={Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles},
|
|
pages={207--220},
|
|
year={2009},
|
|
organization={ACM}
|
|
}
|
|
|
|
@article{Leroy-2009,
|
|
title={Formal verification of a realistic compiler},
|
|
author={Leroy, Xavier},
|
|
journal={Communications of the ACM},
|
|
volume={52},
|
|
number={7},
|
|
pages={107--115},
|
|
year={2009},
|
|
publisher={ACM}
|
|
}
|
|
|
|
@misc{McBride-2005,
|
|
title={Type-preserving renaming and substitution},
|
|
author={McBride, Conor},
|
|
note={unpublished manuscript},
|
|
url={https://personal.cis.strath.ac.uk/conor.mcbride/ren-sub.pdf},
|
|
year={2005}
|
|
}
|
|
|
|
@inproceedings{McBride-2015,
|
|
title={Turing-completeness totally free},
|
|
author={McBride, Conor},
|
|
booktitle={International Conference on Mathematics of Program Construction},
|
|
pages={257--275},
|
|
year={2015},
|
|
organization={Springer}
|
|
}
|
|
|
|
@article{McBride-and-McKinna-2004,
|
|
title={The view from the left},
|
|
author={McBride, Conor and McKinna, James},
|
|
journal={Journal of functional programming},
|
|
volume={14},
|
|
number={1},
|
|
pages={69--111},
|
|
year={2004},
|
|
publisher={Cambridge University Press}
|
|
}
|
|
|
|
@inproceedings{O'Connor-2016,
|
|
title={Refinement through restraint: Bringing down the cost of verification},
|
|
author={O'Connor, Liam and Chen, Zilin and Rizkallah, Christine and Amani, Sidney and Lim, Japheth and Murray, Toby and Nagashima, Yutaka and Sewell, Thomas and Klein, Gerwin},
|
|
booktitle={ICFP},
|
|
pages={89--102},
|
|
year={2016}
|
|
}
|
|
|
|
@book{Pierce-2002,
|
|
title={Types and programming languages},
|
|
author={Pierce, Benjamin C},
|
|
year={2002},
|
|
publisher={MIT press}
|
|
}
|
|
|
|
@inproceedings{Pierce-2009,
|
|
title={Lambda, {T}he {U}ltimate {TA}},
|
|
author={Pierce, Benjamin C},
|
|
booktitle={ICFP},
|
|
pages={121--22},
|
|
year={2009}
|
|
}
|
|
|
|
@book{Pierce-et-al-2010,
|
|
title={Software foundations},
|
|
author={Benjamin C Pierce and Chris Casinghino and Marco Gaboardi and Michael Greenberg and C{\u{a}}t{\u{a}}lin Hri{\c{t}}cu and Vilhelm Sj{\"o}berg and Brent Yorgey},
|
|
url={http://www.cis.upenn.edu/bcpierce/sf/current/index.html},
|
|
year={2010}
|
|
}
|
|
|
|
@inproceedings{Pitts-2010,
|
|
title={Step-indexed biorthogonality: a tutorial example},
|
|
author={Pitts, Andrew M},
|
|
booktitle={Dagstuhl Seminar Proceedings},
|
|
year={2010},
|
|
organization={Schloss Dagstuhl-Leibniz-Zentrum f{\~A}$1/4$r Informatik}
|
|
}
|
|
|
|
@article{Plotkin-1977,
|
|
title={LCF considered as a programming language},
|
|
author={Plotkin, Gordon D.},
|
|
journal={Theoretical Computer Science},
|
|
volume={5},
|
|
number={3},
|
|
pages={223--255},
|
|
year={1977},
|
|
publisher={Elsevier}
|
|
}
|
|
|
|
|
|
@article{Rosu-Serbanuta-2010,
|
|
title={An Overview of the {K} Semantic Framework},
|
|
author={Grigore Ro{\c s}u and Traian Florin {\c S}erb{\u a}nu{\c t}{\u a} },
|
|
journal={Journal of Logic and Algebraic Programming},
|
|
volume={79},
|
|
number={6},
|
|
pages={397--434},
|
|
year={2010}
|
|
}
|
|
|
|
@book{Stump-2016,
|
|
title={Verified functional programming in Agda},
|
|
author={Stump, Aaron},
|
|
year={2016},
|
|
publisher={Morgan \& Claypool}
|
|
}
|
|
|
|
@article{Wright-and-Felleisen-1994,
|
|
title={A syntactic approach to type soundness},
|
|
author={Wright, Andrew K and Felleisen, Matthias},
|
|
journal={Information and computation},
|
|
volume={115},
|
|
number={1},
|
|
pages={38--94},
|
|
year={1994},
|
|
publisher={San Diego: Academic Press, c1987-}
|
|
} |