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 metadata

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 : Tuesday, June 29, 2021 - 11:30:04 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. Information and Computation, Elsevier, 2007, 205 (9), pp.1371-1386. ⟨10.1016/j.ic.2007.03.005⟩. ⟨hal-01148282⟩

Share

Metrics

Record views

275

Files downloads

391