- JonPRL An proof refinement logic for computational type theory based on Brouwer-realizability & the verificationist meaning explanation. Inspired by Nuprl. [For up-to-date development, see JonPRL's succes… 95
- primitive-recursive-bars-are-inductive induction for system-t definable bars via escardó's effectful forcing 6
- agda-effectful-forcing Constructive and formal proof of Brouwer's Bar Theorem & Monotone Bar Induction Principle for System T-definable functionals. 4
- aspects-of-cubical-type-theory notes on the fine structure of cubical syntax & dynamics 7
3,112 contributions in the last year
- Pushed 44 commits to jonsterling/aspects-of-cubical-type-theory Aug 24 – Aug 30
2 Pull Requests
11 Issues reported
- Open #12 A new way to do it!
- Closed #11 correct definition of Focus
- Open #65 [internals] merge ctx_ann with ann
- Open #64 Deprecate LCS machine
- Open #10 odd behavior of "kan expansion" suggests different structure
- Open #9 better notation
- Open #8 double check that I've got variance correct
- Open #7 adhere to angiuli/harper metavariable naming conventions?
- Open #62 bugs in LCS machine
- Closed #5 bound parameters in focused term?
- Closed #4 notation to distinguish 1st-order from 2nd-order signature