Skip to content

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

Notifications You must be signed in to change notification settings

fsestini/nbe-weak-stlc

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.

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages