| [1] | Beniamino Accattoli. Proof pearl: Abella formalization of lambda calculus cube property. In Chris Hawblitzel and Dale Miller, editors, Second International Conference on Certified Programs and Proofs, volume 7679 of LNCS, pages 173--187. Springer, 2012. [ bib ] |
| [2] | Beniamino Accattoli, Horace Blanc, and Claudio Sacerdoti Coen. Formalizing Functions as Processes. In Adam Naumowicz and René Thiemann, editors, 14th International Conference on Interactive Theorem Proving (ITP 2023), volume 268 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1--5:21, Dagstuhl, Germany, 2023. Schloss Dagstuhl -- Leibniz-Zentrum für Informatik. [ bib | DOI | http ] |
| [3] | Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A strong call-by-need calculus. Logical Methods in Computer Science, Volume 19, Issue 1, March 2023. [ bib | DOI | http ] |
| [4] | Kaustuv Chaudhuri, Matteo Cimini, and Dale Miller. A lightweight formalization of the metatheory of bisimulation-up-to. In Xavier Leroy and Alwen Tiu, editors, Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs, pages 157--166, Mumbai, India, January 2015. ACM. [ bib | DOI | http ] |
| [5] | Kaustuv Chaudhuri, Leonardo Lima, and Giselle Reis. Formalized meta-theory of sequent calculi for substructural logics. In Workshop on Logical and Semantic Frameworks, with Applications (LSFA), 2016. Post proceedings version to appear; Formalization https://github.com/meta-logic/abella-reasoning. [ bib ] |
| [6] | Matteo Cimini, Dale Miller, and Jeremy G. Siek. Extrinsically typed operational semantics for functional languages. In Laurence Tratt and Juan de Lara, editors, ACM SIGPLAN International Conference on Software Language Engineering (SLE), pages 108--125. ACM SIGPLAN, ACM, November 2020. [ bib | DOI ] |
| [7] | Amy P. Felty, Alberto Momigliano, and Brigitte Pientka. The next 700 challenge problems for reasoning with higher-order abstract syntax representations: Part 2--A survey. J. of Automated Reasoning, 55(4):307--372, 2015. [ bib | DOI ] |
| [8] | Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control. Journal of Functional Programming, 29, 2019. [ bib | .pdf ] |
| [9] | Jonas Kaiser, Brigitte Pientka, and Gert Smolka. Relating system F and λ2: A case study in Coq, Abella and Beluga. In Dale Miller, editor, FSCD 2017 - 2nd International Conference on Formal Structures for Computation and Deduction, pages 21:1--21:19, Oxford, UK, September 2017. [ bib | DOI ] |
| [10] | Alberto Momigliano. A supposedly fun thing I may have to do again: a HOAS encoding of Howe's method. In Proceedings of LFMTP'12, pages 33--42. ACM, 2012. [ bib | DOI ] |
| [11] | Yuting Wang and Gopalan Nadathur. A higher-order abstract syntax approach to verified transformations on functional programs. In P. Thiemann, editor, Programming Languages and Systems. ESOP 2016, number 9632 in LNCS, pages 752--779. Springer, 2016. [ bib | http ] |
| [12] | Yuting Wang. A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs. PhD thesis, University of Minnesota, December 2016. [ bib | http ] |
| [13] | Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. Formalization of a polymorphic subtyping algorithm. In International Conference on Interactive Theorem Proving (ITP 2018), number 10895 in LNCS, pages 604--622, 2018. [ bib | DOI ] |
| [14] | Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. A mechanical formalization of higher-ranked polymorphic type inference. In Proceedings of the ACM on Programming Languages, volume 3 of ICFP, pages 1--29, July 2019. [ bib | DOI ] |
| [15] | Jinxu Zhao. Formalized Higher-Ranked Polymorphic Type Inference Algorithms. PhD thesis, University of Hong Kong, July 2021. [ bib | .pdf ] |
This file was generated by bibtex2html 1.99.