TheoWinterhalter / Formal Type Theory
Programming Languages
Labels
Projects that are alternatives of or similar to Formal Type Theory
A formalization of type theory in Coq
This Coq library formalizes dependent type theory in the style of Per Martin-Löf. The formalization is configurable in the sense that various components can be turned on or off, or be left ambivalent. It is thus easy to instantiate many variants of type theory, such as extensional vs. intensional, with or without universes, etc. The library also formalizes several meta-theorems about type theory.
Requirements
Requirements for compiling the library
The library works with Coq 8.6, and probably with many other recent versions as well, as it does not use any special features of Coq. You may find out about the best way to install Coq at the Coq web site.
To compile the library you need Coq and make
.
Requirements for generating the LaTeX version of rules
In order to generate the LaTeX version of the rules you need Python (either version 2.7 or 3.x) and (obviously) LaTeX, as well as the mathpartir package by Didier Rémy.
Since the mathpartir
package is GNU-licensed, and we do not want a viral license, the
compilation script attempts to download it using the curl
and wget
commands. If
neither is available, you will have
to download mathpartir
manually
and place it in the latex
subfolder of the repository.
Download
The best way to download the library is to clone it from GitHub. If you do not use git (you should) then you can just download the ZIP file of the latest version. Even better, you can fork the repository so that you can easily send us your improvements (see the section on contributions below).
Compiling
To compile the library and the LaTeX version of the rules run
make
from the command line. The library is in the src
subfolder and the PDF with the rules is latex/rules.pdf
.
Specific targets for make
are:
-
clean
-- clean files -
latex/rules.pdf
-- the rules in PDF, the file can be found inlatex/rules.pdf
-
latex/rulesParanoid.pdf
-- the rules in PDF, but with preconditions -
library
-- compile the library only
For example, make latex/rules.pdf
generates the file latex/rules.pdf
.
Using the library
This section briefly describes how the library is structured and how it can be used and extended.
The files
The src
folder contains the Coq files. Here is an overview of what is in them:
-
config.v
-- configuration options -
config_tactics.v
-- tactics for dealing with configuration options -
ett.v
-- economic type theory -
ett2ptt.v
-- proof that we can pass from economic to paranoid type theory -
ett_sanity.v
-- proof that economic type theory is sane -
inversion.v
-- inversion lemmas -
negfunext.v
-- proof that function extensionality is not provable in MLTT -
ptt.v
-- paranoid type theory -
ptt2ett.v
-- proof that we can pass from paranoid to economic type theory -
ptt_admissible.v
-- various admissibility lemmas for paranoid type theory -
ptt_inversion.v
-- inversion principles for paranoid type theory -
ptt_sanity.v
-- proof that paranoid type theory is sane -
substitution_elim.v
-- an attempt to show that explicit substitutions can be computed -
syntax.v
-- definition of presytnax -
tactics.v
-- tactics for working with the library -
tt.v
-- all the rules of type theory -
uniqueness.v
-- proof of uniqueness of typing
Git branches
The current version of the library is on the master
branch, the rest is kept around for legacy:
-
master
contains the current status of the translation (sanity is being handled, as well as uniqueness of typing), -
zero-shift
contains another formulation of type theory where substitutions have context annotations (probably a bad idea) -
simpler-substitutions
removes all annotations from substitutions but this results in the loss of uniqueness of typing, -
faster-magic
is its counter-part and maybe should be kept instead ofsimpler-substitutions
, -
untyped-refl
corrresponds to an experiment regarding the removal of typing annotation torefl
, -
inversion
corresponds to inversion lemmata (probably subsumed by more recent work), -
into-coq
andinto-coq-attempt
were branches where we were trying to eliminate reflection by translation from our formalised type theory to Coq directly, but e failed. -
bool-disjoint
is about showing thattrue = false -> Empty
(inside the theory), -
bool-large-elim
is about adding large elimination for Bool.
How the library is structured
(To be written)