Alberto Momigliano
ABSTRACT
We formally verify in Abella that similarity in the call-by-name lambda calculus is a pre-congruence, using Howe's method. This turns out to be a very challenging task for HOAS-based systems, as it entails a demanding combination of inductive and coinductive reasoning on open terms, for which no other existing HOAS-based system is equipped for. We also offer a proof using a version of Abella supplemented with predicate quantification; this results in a more structured presentation that is largely independent of the operational semantics as well of the chosen notion of (bi)similarity. While the end result is significantly more succinct and elegant than previous attempts, the exercise highlights some limitations of the two-level approach in general and of Abella in particular.
- Simon Ambler, Roy Crole, and Alberto Momigliano. Combining higher order abstract syntax with tactical theorem proving and (co)induction. In V. A. Carreño, editor, TPHOLs, volume 2342 of LNCS. Springer Verlag, 2002. Google Scholar
Digital Library
- Simon Ambler and Roy L. Crole. Mechanized operational semantics via (co)induction. In Yves Bertot, Gilles Dowek, André Hirschowitz, C. Paulin, and Laurent Théry, editors, TPHOLs, volume 1690 of Lecture Notes in Computer Science, pages 221--238. Springer, 1999. Google ScholarDigital Library
- Brian E. Aydemir et al. Mechanized metatheory for the masses: the poplmark challenge. In Joe Hurd and T. Melham, editors, Theorem Proving in Higher Order Logics, 18th International Conference, Lecture Notes in Computer Science, pages 50--65. Springer, 2005. Google ScholarDigital Library
- James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. J. Log. Comput., 21(6):1177--1216, 2011. Google ScholarDigital Library
- Alberto Ciaffaglione. A coinductive semantics of the unlimited register machine. In Fang Yu and Chao Wang, editors, INFINITY, volume 73 of EPTCS, pages 49--63, 2011.Google Scholar
- Nils Anders Danielsson. Operational semantics using the partiality monad. Agda Implementors' Meeting XI, Awaji Yumebutai, 2010.Google Scholar
- Amy Felty and Brigitte Pientka. Reasoning with higher-order abstract syntax and contexts: A comparison. In ITP 2011, volume 6172 of LNCS, pages 227--242. Springer, 2010. Google ScholarDigital Library
- Amy P. Felty and Alberto Momigliano. Hybrid: A definitional two-level approach to reasoning with higher-order abstract syntax. Journal of Automated Reasoning, 48(1):43--105, 2012. Google ScholarDigital Library
- Jonathan Ford and Ian A. Mason. Formal foundations of operational semantics. Higher-Order and Symbolic Computation, 16(3):161--202, 2003. Google ScholarDigital Library
- Andrew Gacek. A Framework for Specifying, Prototyping, and Reasoning about Computational Systems. PhD thesis, University of Minnesota, September 2009. Google ScholarDigital Library
- Andrew Gacek, Dale Miller, and Gopalan Nadathur. Reasoning in Abella about structural operational semantics specifications. Electr. Notes Theor. Comput. Sci., 228:85--100, 2009. Google ScholarDigital Library
- Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Inf. Comput., 209(1):48--73, 2011. Google ScholarDigital Library
- Furio Honsell, Marino Miculan, and Ivan Scagnetto. ∏-calculus in (co)inductive type theories. Theoretical Computer Science, 2(253):239--285, 2001. Google ScholarDigital Library
- D. J. Howe. Equality in lazy computation systems. In Proceedings of the 4th IEEE Symposium on Logic in Computer Science, pages 198--203, 1989. Google ScholarDigital Library
- Douglas J. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 124(2):103--112, 1996. Google ScholarDigital Library
- Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis. The marriage of bisimulations and kripke logical relations. In John Field and Michael Hicks, editors, POPL, pages 59--72. ACM, 2012. Google ScholarDigital Library
- S. B. Lassen. Relational Reasoning about Functions and Nondeterminism. PhD thesis, Dept of Computer Science, Univ of Aarhus, 1998.Google Scholar
- Xavier Leroy and Hervé Grall. Coinductive big-step operational semantics. Inf. Comput., 207(2):284--304, 2009. Google ScholarDigital Library
- Raymond McDowell and Dale Miller. Reasoning with higher-order abstract syntax in a logical framework. ACM Transactions on Computational Logic, 3(1):80--136, January 2002. Google ScholarDigital Library
- Alberto Momigliano, Simon Ambler, and Roy L. Crole. A Hybrid encoding of Howe's method for establishing congruence of bisimilarity. Electr. Notes Theor. Comput. Sci., 70(2), 2002.Google Scholar
- Keiko Nakata and Tarmo Uustalu. Trace-based coinductive operational semantics for while. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, TPHOLs, volume 5674 of Lecture Notes in Computer Science, pages 375--390. Springer, 2009. Google ScholarDigital Library
- Keiko Nakata and Tarmo Uustalu. Resumptions, weak bisimilarity and big-step semantics for while with interactive I/O: An exercise in mixed induction-coinduction. In Luca Aceto and Pawel Sobocinski, editors, SOS, volume 32 of EPTCS, pages 57--75, 2010.Google Scholar
- Nominal Methods Group. Nominal Isabelle. isabelle.in.tum.de/nominal, 2008, Accessed Sun Feb 14 2010.Google Scholar
- A. M. Pitts. Operationally Based Theories of Program Equivalence. In P. Dybjer and A. M. Pitts, editors, Semantics and Logics of Computation, 1997.Google ScholarCross Ref
- A. M. Pitts. Howe's method for higher-order languages. In D. Sangiorgi and J. Rutten, editors, Advanced Topics in Bisimulation and Coinduction, volume 52, chapter 5, pages 197--232. Cambridge University Press, November 2011.Google ScholarCross Ref
- Alwen Tiu and Dale Miller. Proof search specifications of bisimulation and modal logics for the π-calculus. ACM Trans. Comput. Logic, 11(2):1--35, 2010. Google ScholarDigital Library
- Alwen Tiu and Alberto Momigliano. Cut elimination for a logic with induction and co-induction. CoRR, abs/1009.6171, 2010.Google Scholar
- Philip Wadler, Walid Taha, and David B. MacQueen. How to add laziness to a strict language withouth even being odd. In Proceedings of the 1998 ACM Workshop on ML, pages 24--30, Baltimore, 1998.Google Scholar
Index Terms
- A supposedly fun thing i may have to do again: a HOAS encoding of Howe's method
Recommendations
A Lightweight Formalization of the Metatheory of Bisimulation-Up-To
CPP '15: Proceedings of the 2015 Conference on Certified Programs and ProofsBisimilarity of two processes is formally established by producing a bisimulation relation that contains those two processes and obeys certain closure properties. In many situations, particularly when the underlying labeled transition system is ...
Mechanising Hankin and Barendregt using the Gordon-Melham axioms
MERLIN '03: Proceedings of the 2003 ACM SIGPLAN workshop on Mechanized reasoning about languages with variable bindingI describe the mechanisation in HOL of some basic λ-calculus theory, using the axioms proposed by Gordon and Melham [4]. Using these as a foundation, I mechanised the proofs from Chapters 2 and 3 of Hankin [5] (equational theory and reduction theory), ...
A definitional approach to primitivexs recursion over higher order abstract syntax
MERLIN '03: Proceedings of the 2003 ACM SIGPLAN workshop on Mechanized reasoning about languages with variable bindingIt is well known that there are problems associated with formal systems which attempt to combine higher order abstract syntax (HOAS) with principles of induction and recursion. We describe a formal system, called Bsyntax, which we have implemented in ...
Comments