Abstract
This paper presents a system for explicit substitutions in Pure Type Systems (PTS). The system allows to solve type checking, type inhabitation, higher-order unification, and type inference for PTS using purely first-order machinery. A novel feature of our system is that it combines substitutions and variable declarations. This allows as a side-effect to type check let-bindings. Our treatment of meta-variables is also explicit, such that instantiations of meta-variables is internalized in the calculus. This produces a confluent λ-calculus with distinguished holes and explicit substitutions that is insensitive to α-conversion, and allows directly embedding the system into rewriting logic.
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
Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit substitution. Journal of Functional Programming 1(4), 375–416 (1991)
Barendregt, H.: Lambda calculi with types. In: Gabbai, Abramski, Maibaum (eds.) Handbook of Logic in Comp. Sci., Oxford Univ. Press, Oxford (1992)
Bloo, R.: Preservation of Termination for Explicit Substitution. PhD thesis, Eindhoven University of Technology (1997)
Bloo, R., Kamareddine, F., Nederpelt, R.: The Barendregt cube with definitions and generalised reduction. Inf. and Computation 126(2), 123–143 (1996)
Bognar, M., de Vrijer, R.: The context calculus λ-c. In: LFM 1999: Proceedings of Workshop on Logical Frameworks and Meta-languages (1999)
Bonelli, E.: The polymorphic λ-calculus with explicit substitutions. In: Proc. of 2nd Intl. Workshop on Explicit Substitutions (1999)
Braga, C., Haeusler, H., Meseguer, J., Mosses, P.: Maude action tool: Using reflection to map action semantics to rewriting logic (2000) (submitted)
Coquand, C., Coquand, T.: Structured Type Theory. In: Proc. of Workshop on Logical Frameworks and Meta-Languages (September 1999)
Curien, P.-L., Hardin, T., Lévy, J.-J.: Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM 43(2), 362–397 (1996)
Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions. In: Proc. of LICS, pp. 366–374 (1995)
Dowek, G., Hardin, T., Kirchner, C., Pfenning, F.: Unification via explicit substitutions: The case of higher-order patterns. In: Proc. of LICS (1996)
Elliott, C.: Higher-order unification with dependent types. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 121–136. Springer, Heidelberg (1989)
Geuvers, H.: The Church-Rosser property for βη-reduction in typed λ-calculi. In: Proc. of LICS, pp. 453–460 (1992)
Geuvers, H.: Logics and Type Systems. PhD thesis, Kath. Univ. Nijmegen (1993)
Harper, R., Pfenning, F.: On Equivalence and Canonical Forms in the LF Type Theory. In: LFM 1999: Proc. of Workshop on Logical Frameworks and Metalanguages (1999)
Huet, G.: A unification algorithm for typed λ-calculus. Th. C. S. 1(1), 27–57 (1975)
Luo, Z.: An Extended Calculus of Constructions. Phd thesis CST-65-90, Lab. for Foundations of C. S., Dept. of C. S., Univ. of Edinburgh (July 1990)
Magnusson, L.: The Implementation of ALF−A Proof Editor Based on Martin- Löf’s Monomorphic Type Theory with Explicit Substitution. PhD thesis, Chalmers and Göteborg Univ. (1995)
Mellies, P.A.: Typed λ-calculi with explicit substitutions may not terminate. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, Springer, Heidelberg (1995)
Muñoz, C.: Un calcul de substitutions pour la représentation de preuves partielles en théorie de types. Thèse de doctorat, Université Paris VII (1997)
Muñoz, C., Bjørner, N.: Absolute explicit unification (manuscript), Available from http://www.icase.edu/~munoz/ (July 2000)
Pfenning, F.: Unification and anti-unification in the calculus of constructions. In: Proc. of LICS, pp. 74–85 (1991)
Ríos, A.: Contributions à l’étude de λ-calculs avec des substitutions explicites. Thèse de doctorat, Université Paris VII (1993)
Severi, P., Poll, E.: Pure type systems with defn’s. In: Matiyasevich, Y.V., Nerode, A. (eds.) LFCS 1994. LNCS, vol. 813, pp. 316–330. Springer, Heidelberg (1994)
Stehr, M.-O., Meseguer, J.: Pure type systems in rewriting logic. In: Proceedings of LFM 1999: Workshop on Logical Frameworks and Meta-languages (September 1999)
Strecker, M.: Construction and Deduction in Type Theories. PhD thesis, Univ. Ulm (1999)
Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae 24, 89–105 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bjørner, N., Muñoz, C. (2000). Absolute Explicit Unification. In: Bachmair, L. (eds) Rewriting Techniques and Applications. RTA 2000. Lecture Notes in Computer Science, vol 1833. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721975_3
Download citation
DOI: https://doi.org/10.1007/10721975_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67778-9
Online ISBN: 978-3-540-44980-5
eBook Packages: Springer Book Archive