The POPLmark Challenge is a set of problems about the metatheory of a variant of Sistem F<: The first task of the Challenge concerns its type language (without record types, here):
S,T ::= Top Gamma ::= emptyset | X | Gamma, X<:T | S->T | forall X<:S.TPrecisely, it is required to prove that algorithmic subtyping,
Gamma |- S<:T
, satisfies what follows:
Reflexivity: Gamma |- S<:S Transitivity: Gamma |- S<:Q /\ Gamma |- Q<:T => Gamma |- S<:T Narrowing: Gamma,X<:Q,Delta |- M<:N /\ Gamma |- P<:Q => Gamma,X<:P,Delta |- M<:Nwhere the last two properties have to be proved together, by induction on the structure of the type
Q
.
We address the task by using the proof assistant Coq, and via the following encoding choices:
Our research has been published at LSFA 2012, and the Coq script is available [here].
Afterwards (May 2014), we have provided an alternative, shallow encoding of the same object system.
Finally (March 2015), we have merged the two developments.