[POPLmark] A theory of System-F in Isabelle/HOL

[Dimitrios Vytiniotis]

Hi all,
I have a formalization of System-F in Isabelle/HOL together
with a proof of termination of reduction (which is a small-step
call-by-value one) based on a logical relation argument (the
reducibility candidates technique).

   http://www.cis.upenn.edu/~dimitriv/poplmark/FTheory.tgz
   http://www.cis.upenn.edu/~dimitriv/poplmark/Fmain.pdf
   (document provided for people who cannot run the Isar script
    on Proof General)

Characteristics of this formalization are:

  - Usage of locally-nameless technique (with 2 independent
    de-Bruijn pointer sets for type and term bound variables,
    and names for type and term free variables). I first
    considered pure de-Bruijn representation but gave up pretty quickly
    (after a few dozens of lemmas) because of the fiddling proofs
    that were bringing environments/substitutions/mappings,
    terms and types in sync. Much easier with locally-nameless.

  - The logical relation is defined as a simple recursive function
    with metric the size of types. The reason I did not define it
    structurally is because when we go under a forall quantifier
    we 'freshen' the bound variable with a new name: the type is
    not structurally smaller but has smaller size.

  - I followed much of the initial setup of Xavier Leroy's solution
    to the POPLmark challenge. (thanks!)

  - The price to pay for named free variables are proofs of equivariance
    for most of the relations I defined. I did not find this as bad as
    doing proofs about shifting/crossing quantifiers in a pure de-Bruijn
    setting.

Problems/drawbacks:
(which I eventually plan to fix, towards the end of the summer)

  - My attempt is a brute-force one. I didn't think enough about how to
    make proofs more elegant and less (/more?) verbose (actually I did
    not want some parts that required complicated and interesting
    reasoning to be done automatically either---it's better to know how
    I proved it by looking at the script). Please do not consider this
    proof for immediate conclusions on the proof assistant it is
    implemented in.

  - The code is not yet commented, hopefully the Isar scripts are
    readable enough for a first pass. In the meanwhile I can answer
    specific questions.


Hopefully there are not any problems in the formalization/encoding---if
you do spot one I'd be happy to hear about it and fix it.

Regards,
--dimitris

ps: You will need a recent development snapshot of Isabelle (post
January 2006) to compile this theory. Contact me if you have any trouble
with compilation.