This archive contains formal proofs accompanying the paper

  Tillmann Rendel, Klaus Ostermann and Christian Hofer
  Typed Self-Representation
  PLDI '09

== TECHNICALITIES ==

The proofs can be checked with the Coq proof assistant, version 8.1pl3,
which can be downloaded from http://coq.inria.fr/.

The proofs use the Metatheory library, version 2008-07-17,
which can be downloaded from http://www.cis.upenn.edu/~plclub/metalib/.

To check and compile all proofs, the included makefile can be used. 
Alternatively, the included build_all.bat contains all needed calls to
coqc in the appropriate order. The *.vo files from compiling the Metatheory
library have to be in coq's search path for this to work.

== OVERVIEW OF FILES ==

The following files are included:

Common.v contains common imports, and some notations and tactics

Syntax.v contains the representation of Fomega* terms and types, opening, 
  closing and substitution as well as notations for all of these
  
Tactics.v contains our instantiation of the "pick fresh x" family of tactics
  for working with cofinite quantification, as well as some additional tactics

Infrastructure.v contains low-level technical lemmas about the interaction
  of opening, closing, substitution, free variables etc. 
  
TypBeta.v contains the definition of and lemmas about beta-reduction and 
  beta equivalence on the type and kind level

ExpBeta.v contains the definition of and lemmas about beta-reduction and 
  beta equivalence on the expression level

Kinding.v contains the definition of the kinding relation, written 
  E |- T :: K  in the paper, as well as some of its properties

Simpl.v contains the tactic simpl_exp which tries to simplify an expression
  or a type using facts about opening, closing and substitution

Typechecker.v contains tactics for solving goals about kinding and well-formed
  environments

Typing.v contains the definition of the typing relation, written
  E |- t : T in the paper, as well as some of its properties

Quoting.v contains the definition of the quoting relation, written
  E |- t : T |> t' in the paper, as well as some of its properties

LanguageInterface.v contains the definition of the language interface

Lifting.v contains the notion of lifting an environment, as needed for 
  Lemma 2 in the paper

SelfInterpreter.v contains the definition of the self interpreter, as 
  well as the proof of Lemma 3 and Theorem 5 from the paper. 

Fostar.v contains the proofs of Lemma 2 and Theorem 4 from the paper.

== INTERESTING LEMMAS ==

The following lemmas proof high-level results which are directly mentioned 
in the paper:

lemma_2 in Fostar.v corresponds to Lemma 2 in the paper.

theorem_4 in Fostar.v corresponds to Theorem 4 in the paper.

self_interpretation_a and self_interpretation_b in SelfInterpreter.v together 
  correspond to Lemma 3 and Theorem 5 in the paper. In the formalization, 
  we have a  slightly different distribution of work between the two lemmas
  then in the paper.

kinding_kinding and kinding_typing in Fostar.v formalize the relation between
syntactic categories in Fomega* and kinds in its PTS incarnation, as mentioned
in Section 4 of the paper, "However, it is easy to see that the omitted checks
are syntactically ensured in Fomega*". 

kinding_subst in Kinding.v and typing_subst in Typing.v proof substitution
lemmas for the kinding and typing relations. 

The Coq formalization is completely self-contained and does not rely on the
embedding into the PTS framework.