Skip to content

A library and case-study for linear, intrinsically-typed interpreters in Agda

License

Notifications You must be signed in to change notification settings

metaborg/linear.agda

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Linear, Intrinsically-Typed Interpreters

An Agda library for programming with separation logic, based on proof-relevant separation algebras. The code is organized as follows:

└── src
    ├── Everything.agda       Development entrypoint
    ├── Relation
    │   └── Ternary           The library
    ├── Sessions              Session-types case study
    │   ├── Semantics.agda
    │   ├── Syntax.agda
    │   ├── ...
    ├── Typed
    │   ├── LTLC.agda         LTLC semantics
    │   ├── LTLCRef.agda      LTLCRef semantics

The code has been type-checked using Agda 2.6.0.1. The standard library version that was used is included in lib/.

Agda is usually developed in Emacs. It is highly recommended to use Agda's emacs mode to typecheck the code. This does not only provide type-sensitive highlighting, but also allows you to navigate the code by jumping to definitions.

About

A library and case-study for linear, intrinsically-typed interpreters in Agda

Resources

License

Stars

Watchers

Forks

Packages

No packages published