# Overview

Atlassian Sourcetree is a free Git and Mercurial client for Windows.

Atlassian Sourcetree is a free Git and Mercurial client for Mac.

# Normalization by Evaluation for Martin-Löf Type Theory

A Coq formalization of normalization by evaluation for Martin-Löf dependent type theory equipped with one universe, judgemental equality with η-rules for functional types and the unit type. This formalization leads to certified implementations of procedures for normalization and deciding equality for terms.

Our work formalizes formulation of NbE developed by:

**Normalization by Evaluation for Martin-Löf Type Theory with One Universe**- by Andreas Abel, Klaus Aehlig, Peter Dybjer
- MFPS 2007

**Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements**- by Andreas Abel, Thierry Coquand, Peter Dybjer
- LICS 2007

**A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance**- by Andreas Abel, Thierry Coquand, Miguel Pagano
- TLCA 2009

**Towards Normalization by Evaluation for the βη-Calculus of Constructions**- by Andreas Abel
- FLOPS 2010

## Authors

- Pawel Wieczorek pawel.wieczorek@cs.uni.wroc.pl
- Dariusz Biernacki dabi@cs.uni.wroc.pl

## Setup

Project works with Coq 8.6.1. The required configuration to compile the project is
present in `_CoqProject`

file in the root directory. Inside the source code you can find
other `_CoqProject`

files, but they contain only a file-system-to-coq-module mapping
required by CoqIDE to work without command line parameters. Thus the project
should be compiled from the main directory.

For compilation just type the `coq_makefile -f _CoqProject -o Makefile`

command and then
run the `make`

command.

## Structure of the source code

The source code is located in the `Nbe`

directory which is mapped as the `Nbe`

coq
module.

The formalization of the type system is present in the `./Nbe/Syntax`

directory. the
language of the type theory is presented in the file `Def.v`

. There are two formulations
of the type system. The first one is in the file `System.v`

and the second one is in the
file `SystemN.v`

. It is an augmented duplication that allows to formulate a well-founded
induction princinple.

The directory `./Nbe/Domain`

contains definition of a domain where expressions are
evaluated. Modules `Eval`

, `Nbe`

, `Rb`

contains a graphs of partial
functions used to normalize expressions.

The directory `./Nbe/CodeExtraction`

contains modules responsible for extraction.
The modules `Eval`

, `Nbe`

, `Rb`

contains an encoding of partial functions. The
theoreical results are connected to partial functions in the module `Typed`

and there
you can find functions which are extracted. See *Extracted code* section in this README.

The directory `./Nbe/Model`

contains a formalization of the PER-model. The modules in
this directory contain definitions for conrecete PERs modeling types and basic
properties.

The directory `./Nbe/SoundessOfJudgements`

contains a proof that judgements of
the formalized system are valid in the PER-model. The `Validity`

module contains
a definition of being-valid-in-the-model relation. To manage large numbers of typing rules
we spread parts of the proof to auxiliary modules. The `Soundness`

module contains
the main theorem.

Inside the module `./Nbe/CompletenessOfNbe`

you can find proofs of the completeness
property of the NbE procedure. It is a direct consequence of `SoundnessOfJudgements`

.

The directory `./Nbe/LogicalRelations`

provides logical relations -- a bridge between
syntactic and semantic worlds. All the defintiions are in the `Def`

module. The main
properties are proved in the modules `ClosedUnderPer`

, `ClosedUnderConvertion`

, and
`ConvertibleToReification`

, while the Fundamental Theorem for logical relations is proved
in `FundamentalTheorem`

. Again, to handle proofs of large size we spread particular
cases over many files in dedicated subdirectories.

In the `./Nbe/SoundnessOfNbe`

module the soundness property of the NbE procedure is
proved.

In `./Nbe/Final/Consistency.v`

the consistency of the type system is proved.

`./Nbe/Utils/`

is a collection of loosely related modules containing various auxiliary
definitions.

## Extracted code

The code is extracted into the file `./Code/Extracted.hs`

. The most important parameters
of the extraction mechanism are set in `./Nbe/CodeExtraction/GlobalParameters.v`

.
The extraction is triggered in the `./Nbe/CodeExtraction.v`

file.

The file `Code/Tests.hs`

contains a small collection of test cases for the extracted
normalization procedure.