Abstract
Proof assistants based on type theories, such as COQ and Lego, allow users to omit subterms on input that can be inferred automatically. While those mechanisms are well known, ad-hoc algorithms are used to suppress subterms on output. As a result, terms might be printed identically although they differ in hidden parts. Such ambiguous representations may confuse users. Additionally, terms might be rejected by the type checker because the printer has erased too much type information. This paper addresses these problems by proposing effective erasure methods that guarantee successful term reconstruction, similar to the ones developed for the compression of proof-terms in Proof-Carrying Code environments. Experiences with the implementation in Typelab proved them both efficient and practical.
This research has partly been supported by the “Deutsche Forschungsgemeinschaft” within the “Schwerpunktprogramm Deduktion”.
Acknowledgments
I thank Martin Strecker for developing large parts of the Typelab 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.
Similar content being viewed by others
References
B. Barras et al. The Coq proof assistant reference manual-Version 6.3.1. Technical report, INRIA, France, 1999.
S. Berghofer, T. Nipkow. Proof terms for simply typed higher order logic. In Proc. of TPHOLs’00, volume 1869 of LNCS, pp. 38–53. Springer, 2000.
Th. Coquand, G. Huet. The Calculus of Constructions. Information and Computation, 76(2/3):95–120, 1988.
H. Geuvers. The Church-Rosser property for βη-reduction in typed λ-calculi. In Proc. of LICS’92, pp. 453–460. IEEE Press, 1992.
W. O. D. Griffoen, M. Huisman. A comparison of PVS and Isabelle/HOL. In Proc. of TPHOLs’98, volume 1479 of LNCS, pp. 123–142. Springer, 1998.
W. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225–230, 1981.
M. Hagiya, Y. Toda. On implicit arguments. Technical Report TR-95-1, Department of Information Science, University of Tokyo, 1995.
G. Huet. The Constructive Engine. In A Perspective in Theoretical Computer Science. World Scientific Publishing, Singapore, 1989.
Z. Luo, R. Pollack. LEGO Proof Development System. University of Edinburgh, 1992. Technical Report ECS-LFCS-92-211.
O. Lee, K. Yi. Proofs about a folklore let-polymorphic type inference algorithm. ACM TOPLAS, 20(4):707–723, 1998.
D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. J. Logic Comput., 1(4):497–536, 1991.
A. Miquel. The implicit calculus of constructions. In Proc. of the Conf. TLCA’01, Krakow, Poland, May 2-5, 2001, LNCS. Springer, Berlin, 2001.
C. Muñoz. Proof-term synthesis on dependent-type systems via explicit substitutions. Theoretical Computer Science, 2001. To appear.
G. Necula, P. Lee. Efficient representation and validation of proofs. In Proc. of LICS’98, pp. 93–104. IEEE Press, 1998.
R. Pollack. Implicit syntax. In G. Huet, G. Plotkin, eds., Informal Proc. Of the 1st Workshop on Logical Frameworks (LF’90), Antibes. 1990.
F. Pfenning, C. Schürmann. Algorithms for equality and unification in the presence of notational definitions. In T. Altenkirch, W. Naraschewski, B. Reus, eds., Proc. of TYPES’98, volume 1657 of LNCS, pp. 179–193. Springer, 1999.
B. Pierce, D. Turner. Local type inference. In Conf. Record of POPL’98, pp. 252–265. ACM Press, 1998.
M. Strecker, M. Luther, F. von Henke. Interactive and automated proof construction in type theory. In W. Bibel, P. Schmitt, eds., Automated Deduction — A Basis for Applications, volume I, chapter 3. Kluwer, 1998.
M. Strecker. Construction and Deduction in Type Theories. Ph. D. thesis, Fakultôt für Informatik, Universitôt Ulm, 1999. http://www.informatik.uni-ulm.de/ki/Strecker/phd.html
F. von Henke, M. Luther, M. Strecker. Typelab: An environment for modular program development. In M. Bidoit, M. Dauchet, eds., Proc. of the 7th Intl. Conf. TAPSOFT’97, volume 1214 of LNCS, pp. 851–854. Springer, 1997.
J. B. Wells. Typability and type checking in System F are equivalent and undecidable. Ann. Pure ℰ Appl. Logics, 98(1-3):111–156, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Luther, M. (2001). More On Implicit Syntax. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_31
Download citation
DOI: https://doi.org/10.1007/3-540-45744-5_31
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42254-9
Online ISBN: 978-3-540-45744-2
eBook Packages: Springer Book Archive