Hopper: a sound modern language for computation and transactional resource logic
The aim of Hopper is to provide a logically-sound language for describing ownership, authorization, and transactional interactions thereof. Hopper will also be a nice language for programming and theorem proving.
Hopper is being designed to support both standalone execution and safe program execution embedded within a host application (such as Juno).
What's where
src/contains the Haskell implementation.models/contains formalizations of semantics, and some design experiments that are currently not being used in the implementation.
Contributing
Awesome, lets talk! We can be found on the #hopper channel on freenode.
Good background reading
- Our core IR is derived from the Types Are Calling Conventions paper, which we're augmenting with fancier types.
- As a starting point for combining linear and dependent types, we're drawing from some excellent pre-publication draft work.
- For a good exposition of classical linear logic, see Girard's Linear Logic: its syntax and semantics.
- For a sketch of pattern matching for linearly-typed data structures, see the Copatterns paper.
Build Guide
Read the Build Guide and if it doesn't work, please file a ticket that describes any issues you're facing.