csci8980-f21/papers/scp/PLFA.bib

@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{Aydemir-et-al-2005,
  title={Mechanized metatheory for the masses: the PoplMark challenge},
  author={Aydemir, Brian E and Bohannon, Aaron and Fairbairn, Matthew and Foster, J Nathan and Pierce, Benjamin C and Sewell, Peter and Vytiniotis, Dimitrios and Washburn, Geoffrey and Weirich, Stephanie and Zdancewic, Steve},
  booktitle={International Conference on Theorem Proving in Higher Order Logics},
  pages={50--65},
  year={2005},
  organization={Springer}
}                  


@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}
}

@inproceedings{Owens-et-al-2016,
  title={Functional big-step semantics},
  author={Owens, Scott and Myreen, Magnus O and Kumar, Ramana and Tan, Yong Kiam},
  booktitle={European Symposium on Programming},
  pages={589--615},
  year={2016},
  organization={Springer}
}                  

@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-}
}


@article{Abadi-1991,
	Author = {Abadi, M. and Cardelli, L. and Curien, P.-L. and Levy, J.-J.},
	Journal = {Journal of Functional Programming},
	Number = {4},
	Pages = {375-416},
	Title = {Explicit Substitutions},
	Volume = {1},
	Year = {1991}}


@book{Barendregt-1984,
	Author = {H.P. Barendregt},
	Publisher = {Elsevier},
	Series = {Studies in Logic},
	Title = {The Lambda Calculus},
	Volume = {103},
	Year = {1984}}


@inproceedings{Schafer-Tebbi-Smolka-2015,
	Author = {Steven Sch{\"{a}}fer and Tobias Tebbi and Gert Smolka},
	Booktitle = {Interactive Theorem Proving - 6th International Conference},
	Month = {August},
	Pages = {359--374},
	Publisher = {Springer},
	Series = {ITP},
	Title = {Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions},
	Year = {2015}}


@techreport{Pfenning-1992,
	Address = {Pittsburgh, PA, USA},
	Author = {Pfenning, Frank},
	Institution = {Carnegie Mellon University},
	Number = {CMU-CS-92-186},
	Title = {A Proof of the Church-Rosser Theorem and Its Representation in a Logical Framework},
	Year = {1992}}


@article{Siek-2017,
	Author = {Jeremy G. Siek},
	Journal = {CoRR},
	Number = {4},
	Title = {Revisiting Elementary Denotational Semantics},
	Volume = {abs/1707.03762},
	Year = {2017}}


@article{Scott-1976,
	Author = {Dana Scott},
	Journal = {SIAM Journal on Computing},
	Number = {3},
	Pages = {522-587},
	Title = {Data Types as Lattices},
	Volume = {5},
	Year = {1976}}


@article{Engeler-1981,
	Author = {Engeler, Erwin},
	Journal = {algebra universalis},
	Month = {Dec},
	Number = {1},
	Pages = {389--392},
	Title = {Algebras and combinators},
	Volume = {13},
	Year = {1981}}


@article{Plotkin-1993,
	Author = {Gordon D. Plotkin},
	Journal = {Theoretical Computer Science},
	Number = {1},
	Pages = {351 - 409},
	Title = {Set-theoretical and other elementary models of the λ-calculus},
	Volume = {121},
	Year = {1993}}


@article{Barendregt-1983,
	Author = {Henk Barendregt and Mario Coppo and Mariangiola Dezani-Ciancaglini},
	Journal = {Journal of Symbolic Logic},
	Month = {12},
	Number = {4},
	Pages = {931-940},
	Title = {A filter lambda model and the completeness of type assignment},
	Volume = {48},
	Year = {1983}}

@inproceedings{Kokke-2015,
  abstract  = {As proofs in type theory become increasingly
                  complex, there is a growing need to provide better
                  proof automation. This paper shows how to implement
                  a Prolog-style resolution procedure in the
                  dependently typed programming language
                  Agda. Connecting this resolution procedure to Agda’s
                  reflection mechanism provides a first-class proof
                  search tactic for first-order Agda terms. As a
                  result, writing proof automation tactics need not be
                  different from writing any other program. },
  year      = {2015},
  month     = jun,
  isbn      = {978-3-319-19796-8},
  booktitle = {Mathematics of Program Construction},
  volume    = {9129},
  series    = {Lecture Notes in Computer Science},
  editor    = {Hinze, Ralf and Voigtländer, Janis},
  doi       = {10.1007/978-3-319-19797-5_14},
  title     = {Auto in Agda: Programming Proof Search Using Reflection},
  url       = {https://wenkokke.github.io/pubs/mpc2015.pdf},
  publisher = {Springer International Publishing},
  author    = {Wen Kokke and Wouter Swierstra},
  pages     = {276-301}}

@thesis{Kidney-2019,
	address = {Cork, Ireland},
	type = {Bachelor thesis},
	title = {Automatically and {Efficiently} {Illustrating} {Polynomial} {Equalities} in {Agda}},
	url = {https://doisinkidney.com/pdfs/bsc-thesis.pdf},
	abstract = {We present a new library which automates the construction of equivalence proofs between polynomials over commutative rings and semirings in the programming language Agda [20]. It is signi cantly faster than Agda’s existing solver. We use re ection to provide a sim- ple interface to the solver, and demonstrate how to use the constructed proofs to provide step-by-step solutions.},
	language = {en},
	school = {University College Cork},
	author = {Kidney, Donnacha Oisín},
	month = apr,
	year = {2019}}

@incollection{Reynolds-2003,
  title={What do types mean?--From intrinsic to extrinsic semantics},
  author={John C Reynolds},
  booktitle={Programming methodology},
  pages={309--327},
  year={2003},
  publisher={Springer}
}                  

@inproceedings{Wadler-2018,
  author = {Philip Wadler},
  title = {Programming Language Foundations in Agda},
  editors = {Tiago Massoni and Mohammad Mousavi},
  booktitle = {Formal Methods: Foundations and Applications (SBMF 2018)},
  series = {Lecture Notes in Computer Science},
  volume = {11254},
  publisher = {Springer},
  year = {2018}                    
}