This is based on Escardó's "effectful forcing" development. See http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue-lambda.html for the original code and work to which we owe so much!
-
-
Notifications
You must be signed in to change notification settings - Fork 0
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.
jonsterling/agda-effectful-forcing
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
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 0
No packages published