Skip to Main content Skip to Navigation
Journal articles

Intersection-types à la Church

Abstract : In this paper, we present Λ^t_∧, a fully typed λ-calculus based on the intersection-type system discipline, which is a counterpart à la Church of the type assignment system as invented by Coppo and Dezani. The relationship between Λ^t_∧ and the intersection type assignment system is the standard isomorphism between typed and type assignment system, and so the typed language inherits from the untyped system all the good properties, like subject reduction and strong normalization. Moreover both type checking and type reconstruction are decidable.
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-01148282
Contributor : Luigi Liquori <>
Submitted on : Monday, May 4, 2015 - 1:04:18 PM
Last modification on : Saturday, January 27, 2018 - 1:31:34 AM
Long-term archiving on: : Wednesday, April 19, 2017 - 2:22:32 PM

File

2007-ic-07.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Luigi Liquori, Simona Ronchi Della Rocca. Intersection-types à la Church. Journal of Information and Computation, Elsevier, 2007, 205 (9), pp.1371-1386. ⟨10.1016/j.ic.2007.03.005⟩. ⟨hal-01148282⟩

Share

Metrics

Record views

260

Files downloads

327