Skip to content

Agda formalization of the paper, "Higher-Order Functions and Brouwer's Thesis". Deduces a Brouwer ordinal from a function ((nat -> nat) -> nat) in System T.

Notifications You must be signed in to change notification settings

jonsterling/agda-effectful-forcing

Folders and files

NameName
Last commit message
Last commit date

Latest commit

cc99328 · Sep 22, 2020

History

89 Commits
Sep 21, 2020
Sep 22, 2020
Sep 22, 2020
May 9, 2016
Sep 22, 2020
Jan 16, 2018
May 26, 2016
Sep 21, 2020

Repository files navigation

About

Agda formalization of the paper, "Higher-Order Functions and Brouwer's Thesis". Deduces a Brouwer ordinal from a function ((nat -> nat) -> nat) in System T.

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Sponsor this project

Packages

No packages published