ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Tue 9 Apr 2019 12:00 - 12:30 at SUN II - Types Chair(s): Vasco T. Vasconcelos

Adding predicate subtyping to higher-order logic yields a very expressive language in which type-checking is undecidable, making the definition of a system of verifiable certificates challenging. This work presents a solution to this issue with a minimal formalization of predicate subtyping, named PVS-Core, together with a system of verifiable certificates for PVS-Core, named PVS-Cert. PVS-Cert is based on the introduction of proof terms and explicit coercions. Its design is similar to that of PTSs with dependent pairs, at the exception of the definition of conversion, which is based on a specific notion of reduction $\rightarrow_{\beta *}$, corresponding to $\beta$-reduction combined with the erasure of coercions. The use of this reduction instead of the more standard reduction $\rightarrow_{\beta \sigma}$ allows to establish a simple correspondence between PVS-Core and PVS-Cert. On the other hand, a type-checking algorithm is designed for PVS-Cert, built on proofs of type preservation of $\rightarrow_{\beta \sigma}$ and strong normalization of both $\rightarrow_{\beta \sigma}$ and $\rightarrow_{\beta *}$. Using these results, PVS-Cert judgements are used as verifiable certificates for predicate subtyping. In addition, the reduction $\rightarrow_{\beta \sigma}$ is used to define a cut elimination procedure adapted to predicate subtyping. Its use to study the properties of predicate subtyping is illustrated with a proof of consistency.

Tue 9 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30
TypesESOP at SUN II
Chair(s): Vasco T. Vasconcelos University of Lisbon, Portugal
10:30
30m
Talk
Handling polymorphic algebraic effects
ESOP
Taro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University, Japan
Link to publication
11:00
30m
Talk
Distributive Disjoint Polymorphism for Compositional Programming
ESOP
Xuan Bi Standard Chartered Bank, Ningning Xie University of Toronto, Bruno C. d. S. Oliveira The University of Hong Kong, Hong Kong, Tom Schrijvers KU Leuven
Link to publication
11:30
30m
Talk
Types by Need
ESOP
Beniamino Accattoli Inria & Ecole Polytechnique, Giulio Guerrieri University of Bath, Maico Leberle
Link to publication
12:00
30m
Talk
Verifiable certificates for predicate subtyping
ESOP
Link to publication