Publications formalized using Abella

[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] 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 ]
[3] 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 ]
[4] 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 ]
[5] 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 ]
[6] 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. Springer, 2016. [ bib ]
[7] Yuting Wang. A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs. PhD thesis, University of Minnesota, December 2016. [ bib ]

This file was generated by bibtex2html 1.99.