HTTPS SSH

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

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.