MgrCoq /

Filename Size Date modified Message
104 B
1.3 KB
5.0 KB
274 B
11.2 KB
526 B
== Formalization of normalization-by-evaluation for Martin Lof Type Theory with Universe.
== Pawel Wieczorek, University of Wroclaw, Poland

>>> Introduction

This package contains formalization of NBE for dependend type thoery in Martin-Lof style. Main goal of this
project is to provide certified normalizer and decision procedure for term/type equality.

Second goal is to provide well-written package, which could be easy modifiable by other people.

Package is written for Coq 8.4pl3 (February 2014).

>>> Type Theory