GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → metaborg → linear.agda

metaborg / linear.agda

Licence: MIT license
A library and case-study for linear, intrinsically-typed interpreters in Agda

Programming Languages

Agda
84 projects
Makefile
30231 projects

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.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].