Name		Name	Last commit message	Last commit date
Explicit		Explicit
Syntax		Syntax
.gitignore		.gitignore
Correspondence.agda		Correspondence.agda
Decide.agda		Decide.agda
Everything.agda		Everything.agda
Explicit.agda		Explicit.agda
Implicit.agda		Implicit.agda
Normalization.agda		Normalization.agda
README.md		README.md
Utils.agda		Utils.agda

Repository files navigation

nbe-weak-stlc

Agda formalization of normalization by evaluation for the confluent simply-typed weak lambda-calculus.

Companion code to my paper Normalization by Evaluation for Typed Weak lambda-Reduction (link here).

About

Agda formalization of normalization by evaluation for the confluent simply-typed weak lambda-calculus.

agda lambda-calculus normalization-by-evaluation simple-types weak-reduction

8 stars

1 watching

Report repository

Releases

Packages

Contributors

Languages