Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456

Notice: Undefined index: scheme in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 88

Notice: Undefined index: host in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 88

Notice: Undefined index: scheme in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 93
[go: Go Back, main page]
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 ]