Skip to content
This repository has been archived by the owner on Jul 19, 2022. It is now read-only.
/ coc-os Public archive

"operating system" based on the calculus of constructions

Notifications You must be signed in to change notification settings

atennapel/coc-os

Repository files navigation

Try it out at https://atennapel.github.io/coc-os

Run CLI REPL:

yarn install
yarn start

Typecheck file:

yarn install
yarn start filename

Currently done:

  • dependent functions (pi types)
  • dependent pairs (sigma types)
  • an heterogenous equality type with definitional uniqueness of identity proofs (UIP)
  • booleans with an induction primitive
  • type-in-type
  • indexed descriptions ala "Gentle Art of Levitation"
  • generic constructors from "Generic Constructors and Eliminators from Descriptions"
  • generic eliminators from "Generic Constructors and Eliminators from Descriptions" (just for boolean-tagged datatypes for now)
  • named holes (_name)
  • generic eliminators for Fin tagged datatypes
  • explicit erasure annotations

Not yet done:

  • CEK machine for erased terms
  • hash-based content-addressed references
  • IO monad for system calls

Future work:

  • levitation of Desc
  • inductive-recursive types
  • inductive-inductive types
  • predicative universe hierarchy
TODO:
- add native unit type (for better printing, () : {})
- make erased language bigger (ifs, fix, etc.) in order to reduce ugly lambda encodings
- implement instance search
- implement pruning
- specialize meta when checking pair
- allow second component of pair to be erased
- fix infinite loop in postponements
- fix _ being used in elaboration
- allow erased FArg, Rec and HRec
- allow meta as head of glued value
- glued lets
- support some impredicative instantiation
- add a way to not mention type in argument of pi/sigma etc.

QUESTIONS:
- how to levitate in my core theory?
- is a first-order Arg description useful? (IFArg)
- can we erase Unit index in Desc?

LIBRARIES:
- find alternate definitions of symm, trans, eqRefl and uip, to allow for erasure of the proofs
- write more prelude functions
- write Desc using Desc

About

"operating system" based on the calculus of constructions

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published