Abstract
Subsumption used in subtyping breaks the term-as-proofs paradigm. Semantics most naturally are associated with proofs. Thus a problem of coherence arises: different typing proofs of the same term must have related meanings. We propose a proof-theoretical, rewriting approach to this problem. We focus on F≤, a second order lambda calculus with bounded quantification, which is rich enough to make the problem interesting. We define a normalizing rewrite system on the proofs, in which different proofs of the same typing judgement are transformed in a unique normal proof, and in which normal proofs of judgements assigning different types to the same term are strongly related. This rewriting system is not defined on the proofs themselves but on the terms of an auxiliary type system, in which the terms carry a complete information about their typing proof. This technique gives also a simple proof of the existence of a minimum type for each term. From an analysis of the proofs in normal form we obtain a deterministic type-checking algorithm, which is sound and complete by construction.
This work was carried on while this author was visiting DEC SRC, Palo Alto
This work was carried on with the partial support of E.E.C., Esprit Basic Research Action 3070 FIDE and of Italian C.N.R. “Sistemi informatici e calcolo parallelo”
Preview
Unable to display preview. Download preview PDF.
10. References
R. Amadio, “Formal Theories of Inheritance for Typed Functional Languages”, Technical Report, Dipartimento di Informatica, Università di Pisa, Pisa, Italy, 1989.
(BCGS for short) Breazu V., Coquand T., Gunter C., Scedrov A., “Inheritance and Explicit Coercion”, Proc. LICS 89, Monterey, USA, 1989.
(BL for short) Bruce K.B., Longo G., “A Modest Model of Records, Inheritance and Bounded Quantification”, Technical Report TR-7/89, Dipartimento di Informatica, Università di Pisa, Pisa, Italy, 1989.
Cardelli L., Longo G., “A Semantic Basis for Quest”, accepted at Lisp and Functional Programming 90, Nice.
Cardelli L., Wegner P., “On Understanding Types, Data Abstraction and Polymorphism”, ACM Computing Surveys, Dec. 1985.
personal communication
Ghelli G., “The decidability of type checking for Fun”, Technical Report in preparation, Dipartimento di Informatica, Università di Pisa, Pisa, Italy, 1989.
Ghelli G., “Proof-theoretic Studies about a Minimal Type System Integrating Inclusion and Parametric Polymorphism”, PhD Thesis, University of Pisa, February 90.
personal communication.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Curien, PL., Ghelli, G. (1990). Coherence of subsumption. In: Arnold, A. (eds) CAAP '90. CAAP 1990. Lecture Notes in Computer Science, vol 431. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52590-4_45
Download citation
DOI: https://doi.org/10.1007/3-540-52590-4_45
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52590-5
Online ISBN: 978-3-540-47042-7
eBook Packages: Springer Book Archive