Inductive beluga: programming proofs. (English) Zbl 1465.68294
Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9195, 272-281 (2015).
Summary: beluga is a proof environment which provides a sophisticated infrastructure for implementing formal systems based on the logical framework LF together with a first-order reasoning language for implementing inductive proofs about them following the Curry-Howard isomorphism.{
}In this paper we describe four significant extensions to beluga: (1) we enrich our infrastructure for modelling formal systems with first-class simultaneous substitutions, a key and common concept when reasoning about formal systems (2) we support inductive definitions in our reasoning language which significantly increases beluga’s expressive power (3) we provide a totality checker which guarantees that recursive programs are well-founded and correspond to inductive proofs (4) we describe an interactive program development environment. Taken together these extensions enable direct and compact mechanizations. To demonstrate beluga’s strength and illustrate these new features we develop a weak normalization proof using logical relations.
For the entire collection see [Zbl 1316.68011].
For the entire collection see [Zbl 1316.68011].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
References:
| [1] | Savary-Belanger, O.; Monnier, S.; Pientka, B.; Gonthier, G.; Norrish, M., Programming type-safe transformations using higher-order abstract syntax, Certified Programs and Proofs, 243-258 (2013), Heidelberg: Springer, Heidelberg · Zbl 1426.68061 · doi:10.1007/978-3-319-03545-1_16 |
| [2] | Bertot, Y.; Castéran, P., Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions (2004), Heidelberg: Springer, Heidelberg · Zbl 1069.68095 · doi:10.1007/978-3-662-07964-5 |
| [3] | Cave, A., Pientka, B.: Programming with binders and indexed data-types. In: 39th Annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2012), pp. 413-424. ACM Press (2012) · Zbl 1321.68141 |
| [4] | Cave, A., Pientka, B.: First-class substitutions in contextual type theory. In: 8th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2013), pp. 15-24. ACM Press (2013) |
| [5] | Dunfield, J., Pientka, B.: Case analysis of higher-order data. In: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008), Electronic Notes in Theoretical Computer Science (ENTCS 228), pp. 69-84. Elsevier (2009) · Zbl 1337.68058 |
| [6] | Felty, A.P., Momigliano, A., Pientka, B.: The next 700 Challenge Problems for Reasoning with Higher-order Abstract Syntax Representations: Part 2 - a Survey. Journal of Automated Reasoning (2015) · Zbl 1357.68198 |
| [7] | Ferreira, F., Pientka, B.: Bidirectional elaboration of dependently typed languages. In: 16th International Symposium on Principles and Practice of Declarative Programming (PPDP 2014). ACM (2014) |
| [8] | Gacek, A.; Armando, A.; Baumgartner, P.; Dowek, G., The abella interactive theorem prover (System Description), Automated Reasoning, 154-161 (2008), Heidelberg: Springer, Heidelberg · Zbl 1165.68457 · doi:10.1007/978-3-540-71070-7_13 |
| [9] | Gacek, A., Miller, D., Nadathur, G.: Combining generic judgments with recursive definitions. In: 23rd Symposium on Logic in Computer Science. IEEE Computer Society Press (2008) |
| [10] | Girard, J-Y; Lafont, Y.; Tayor, P., Proofs and Types (1990), Cambridge: Cambridge University Press, Cambridge |
| [11] | Harper, R.; Honsell, F.; Plotkin, G., A framework for defining logics, J. ACM, 40, 1, 143-184 (1993) · Zbl 0778.03004 · doi:10.1145/138027.138060 |
| [12] | Magnusson, L.; Nordström, B.; Barendregt, Henk; Nipkow, Tobias, The Alf proof editor and its proof engine, TYPES: Types for Proofs and Programs, 213-237 (1994), Heidelberg: Springer, Heidelberg · Zbl 1527.68259 · doi:10.1007/3-540-58085-9_78 |
| [13] | Nanevski, A.; Pfenning, F.; Pientka, B., Contextual modal type theory, ACM Trans. Comput. Logic, 9, 3, 1-49 (2008) · Zbl 1367.03060 · doi:10.1145/1352582.1352591 |
| [14] | Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D thesis, Department of Computer Science and Engineering, Chalmers University of Technology, September 2007. Technical Report 33D |
| [15] | Pfenning, F.; Schürmann, C.; Ganzinger, H., System description: Twelf - a meta-logical framework for deductive systems, Automated Deduction - CADE-16, 202-206 (1999), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-48660-7_14 |
| [16] | Pientka, B.: A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In: 35th Annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2008), pp. 371-382. ACM Press (2008) · Zbl 1295.68068 |
| [17] | Pientka, B., An insider’s look at LF type reconstruction: Everything you (n)ever wanted to know, J. Funct. Program., 23, 1, 1-37 (2013) · Zbl 1262.68030 · doi:10.1017/S0956796812000408 |
| [18] | Pientka, B., Abel, A.: Structural recursion over contextual objects, In: 13th Typed Lambda Calculi and Applications (TLCA 2015), LIPIcs-Leibniz International Proceedings in Informatics (2015) · Zbl 1367.68073 |
| [19] | Pientka, B.; Dunfield, J.; Giesl, J.; Hähnle, R., Beluga: a framework for programming and reasoning with deductive systems (System Description), Automated Reasoning, 15-21 (2010), Heidelberg: Springer, Heidelberg · Zbl 1291.68366 · doi:10.1007/978-3-642-14203-1_2 |
| [20] | Tait, W., Intensional Interpretations of Functionals of Finite Type I, J. Symb. Log., 32, 2, 198-212 (1967) · Zbl 0174.01202 · doi:10.2307/2271658 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
