lambda-calculus icon indicating copy to clipboard operation
lambda-calculus copied to clipboard

verified publisher icon pi8027
→

Metadata

A Formalization of Typed and Untyped λ-Calculi in Coq and Agda2

Results 1 lambda-calculus issues
Sort by recently updated
recently updated
newest added

Proof of correctness of addition and multiplication of Church numerals in Agda

1 comment

Hi! I was reading _Lectures on the Curry-Howard Isomorphism_ and learning about Church encodings when I thought that proving their correctness would be a fun Agda exercise. Since I didn't...

timjb avatar timjb

← Metadata

75
Stars
7
Forks
Watchers

Owner

verified publisher icon pi8027

Metadata

A Formalization of Typed and Untyped λ-Calculi in Coq and Agda2

Back