Heq
: a Coq library for Heterogeneous Equality.
Chung-Kil Hur
Laboratoire Preuves Programmes Systèmes
CNRS
&
Université Paris Diderot
Tutorial
Library source
Strongly typed representation of System F
Strong normalization of System F
Vector
(cf.
List
in Coq 8.2pl1)
Mergesort of vectors and its correctness
(cf.
Hugo Herberlin's Mergesort of lists and its correctness
)
Download
Source: [
Heq-0.92.zip
(for Coq 8.3pl1) 184 KB]
Publications
Heq: a Coq library for heterogeneous equality
.
Informal presentation at the 2nd Coq Workshop (
Coq 2010
), A satellite workshop of ITP 2010.
[preprint:
pdf
] [slides:
pdf
] [coq script:
script
]