Write a Blog >>
APLAS 2019
Sun 1 - Wed 4 December 2019 Bali, Indonesia
Mon 2 Dec 2019 10:30 - 11:00 at Bali Room - Types Chair(s): Tachio Terauchi

We present a manifest contract system PCFv∆H with intersection types. A manifest contract system is a typed functional calculus in which software contracts are integrated into a refinement type system and consistency of contracts is checked by combination of compile- and run-time type checking. Intersection types naturally arise when a contract is expressed by a conjunction of smaller contracts. Run-time contract checking for conjunctive higher-order contracts in an untyped language has been studied but our typed setting poses an additional challenge due to the fact that an expression of an intersection type τ1 ∧ τ2 may have to perform different run-time checking whether it is used as τ1 or τ2. We build PCFv∆H on top of the ∆-calculus, a Church-style intersection type system by Liquori and Stolze. In the ∆-calculus, a canonical expression of an intersection type is a strong pair, whose elements are the same expressions except for type annotations. To address the challenge above, we relax strong pairs so that expressions in a pair are the same except for type annotations and casts, which are a construct for run-time checking. We give a formal definition of PCFv∆H and show its basic properties as a manifest contract system: preservation, progress, and value inversion. Furthermore, we show that run-time checking does not affect essential computation.

Mon 2 Dec
Times are displayed in time zone: (GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi change

10:30 - 12:00: Research Papers - Types at Bali Room
Chair(s): Tachio TerauchiWaseda University
aplas-2019-papers10:30 - 11:00
Yuki NishidaKyoto University, Atsushi IgarashiKyoto University, Japan
aplas-2019-papers11:00 - 11:30
Akira KawataKyoto University, Atsushi IgarashiKyoto University, Japan
aplas-2019-papers11:30 - 12:00
Raimil CruzUniversity of Chile, Éric TanterUniversity of Chile & Inria Paris