University of Udine University of Udine

A weak HOAS approach to the POPLmark Challenge


Alberto Ciaffaglione, Ivan Scagnetto

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.T
Precisely, 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<:N
where 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.


Last updated: November 20, 2012