GitHub - fsestini/nbe-mltt-wes: Normalization by Evaluation for a version of Martin-Löf Type Theory with weak explicit substitutions. · GitHub

Name		Name	Last commit message	Last commit date
Latest commit History 5 Commits
Semantics		Semantics
Syntax		Syntax
.gitignore		.gitignore
Semantics.agda		Semantics.agda
Syntax.agda		Syntax.agda
Utils.agda		Utils.agda

About

Normalization by Evaluation for a version of Martin-Löf Type Theory with weak explicit substitutions.

lambda-calculus proof-assistant type-theory agda normalization martin-lof normalization-by-evaluation explicit-substitutions

Report repository

Releases 1

release-msc-thesis Latest

Packages

Contributors

Languages

Agda 100.0%