Abstract
Incomplete logical proofs are the logical counterpart of the incomplete λ-terms that one usually works with in an interactive theorem prover based on type theory. In this paper we extend the formalization of such incomplete proofs given in [5] by introducing unknowns that are allowed to provide temporary bindings for variables that are supposed to be bound, but whose binders are not constructed yet — a situation that typically occurs when one does forward reasoning.
We do this by introducing hereditarily parameterized meta-variables and show that by separating the object-level from the meta-level abstractions one can get the abstraction needed to implement the incomplete objects without having to extend the function spaces of the object-level system. We define a typing system that extends λHOL and re-establish the formulas-as-types embedding of the logic with binding holes into this system.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Henk Barendregt. Lambda calculi with types. In Abramsky et al., editor, Handbook of Logic in Computer Science, pages 117–309. Oxford University Press, 1992.
R. Bloo, Fairouz Kamareddine, Twan Laan, and Rob Nederpelt. Parameters in Pure Type Systems. In Proceedings of LATIN’02. Springer, 2002.
Mirna Bognar. Contexts in Lambda Calculus. PhD thesis, VU Amsterdam, 2002.
N.G. de Bruijn. A Survey of the Project AUTOMATH. In Hindley and Seldin, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.
Herman Geuvers and G.I. Jojgov. Open proofs and open terms: a basis for interactive logic. In Bradfield, editor, Proceedings of CSL’02. Springer, 2002.
J.H. Geuvers. Logics and Type systems. PhD thesis, University of Nijmegen.
Zhaohui Luo. PAL+: A lambda-free logical framework. Journal of Functional Programming, to appear.
Lena Magnusson. The Implementation of ALF — a Proof Editor based on Martin-Löf Monomorphic Type Theory with Explicit Substitutions. PhD thesis, Chalmers University of Technology / Göteborg University, 1995.
Conor McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh, 1999.
Dale Miller. Unification under a mixed prefix. J. of Symbolic Computation, 1992.
Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5(3):363–397, 1989.
P. Severi and E. Poll. Pure Type Systems with definitions. In Proc. of LFCS’94, St. Petersburg, Russia, number 813 in LNCS, Berlin, 1994. Springer Verlag.
M. Strecker. Construction and Deduction in Type Theories. PhD thesis, Universität Ulm, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jojgov, G.I. (2003). Holes with Binding Power. In: Geuvers, H., Wiedijk, F. (eds) Types for Proofs and Programs. TYPES 2002. Lecture Notes in Computer Science, vol 2646. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-39185-1_10
Download citation
DOI: https://doi.org/10.1007/3-540-39185-1_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-14031-3
Online ISBN: 978-3-540-39185-2
eBook Packages: Springer Book Archive