Coercions
Coercions
This project is joint work with
Julien Cretin
(linkedin)
and
Gabriel Scherer
Full reduction in the face of absurdity
See the
abstract,
the
ESOP 2015
paper and the
long version.
See also this
talk given at the IFIP WG 2.8 in Kefalonia, Greece, May 2015.
System F with coercion constraints.
See the paper presented at
LICS'2014
[bibtex].
The full version is available as a
research repport
[abstract
bibtex].
The language and the proofs have been formalized and mechanized in Coq
(version 8.4) by Julien Cretin. The scrips can be found
as an annexe to Julien's PhD dissertation.
The essence of the language has also been described in a
presented in
core version
[
bibtex]
presented at
Luca Cardelli Fest.
Coherent Coercion Abstraction with a step-indexed strong-reduction semantics
[ ABSTRACT
| PDF
| BIB
].
The language and the proofs have been formalized and mechanized in Coq
(version 8.4) by Julien Cretin. The scrips can be found
here.
Extending System F with Abstraction over Erasable Coercions
The conference version (POPL 2012) is available here
[ ABSTRACT
| PDF
| BIB
].
A long version with detailed proofs is available on
HAL
as
INRIA Research Report 7587
[ ABSTRACT
| PDF
| BIB
]