michaelsproul / Dblib Linear
Formalisation of the linear lambda calculus in Coq
Stars: ✭ 10
Labels
Projects that are alternatives of or similar to Dblib Linear
Iron
Coq formalizations of functional languages.
Stars: ✭ 114 (+1040%)
Mutual labels: proof, coq, lambda-calculus
Verdi Raft
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
Stars: ✭ 143 (+1330%)
Mutual labels: proof, coq
Disel
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
Stars: ✭ 85 (+750%)
Mutual labels: proof, coq
coq-to-ocaml-to-js
Proof of concept to generate safe and fast JavaScript
Stars: ✭ 25 (+150%)
Mutual labels: coq, proof
system-F
Formalization of the polymorphic lambda calculus and its parametricity theorem
Stars: ✭ 20 (+100%)
Mutual labels: lambda-calculus, coq
InfSeqExt
A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators
Stars: ✭ 12 (+20%)
Mutual labels: coq, proof
imm
Intermediate Memory Model (IMM) and compilation correctness proofs for it
Stars: ✭ 15 (+50%)
Mutual labels: coq, proof
Verdi
A framework for formally verifying distributed systems implementations in Coq
Stars: ✭ 496 (+4860%)
Mutual labels: proof, coq
Unimath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Stars: ✭ 680 (+6700%)
Mutual labels: coq
Micro Policies Coq
Coq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Tag-Based Security Monitors
Stars: ✭ 18 (+80%)
Mutual labels: coq
Fp Core.rs
A library for functional programming in Rust
Stars: ✭ 772 (+7620%)
Mutual labels: lambda-calculus
Autosubst
Automation for de Bruijn syntax and substitution in Coq
Stars: ✭ 22 (+120%)
Mutual labels: coq
Category Theory
An axiom-free formalization of category theory in Coq for personal study and practical work
Stars: ✭ 562 (+5520%)
Mutual labels: coq
Cufp 2015 Tutorial
An introductory tutorial for the Coq proof assistant.
Stars: ✭ 9 (-10%)
Mutual labels: coq
Monads
Coq code accompanying several articles on semantics of functional programming languages
Stars: ✭ 9 (-10%)
Mutual labels: coq
Linear Lambda Calculus using DbLib
This is a mechanical formalisation of a (Purely) Linear Lambda Calculus using the Coq theorem prover.
It makes use of François Pottier's DbLib for de Bruijn indices.
I completed this formalisation as part of my honours thesis in computer science at UNSW.
Source Layout
- DbLib - my fork of DbLib with a few minor changes (lowering added)
- Linear - a collection of universal definitions about context splitting
- Syntax.v - types, terms and substitution for PLLC
- Typing.v - typing judgements for PLLC
- SmallStepSemantics.v - small-step operational semantics for PLLC
- Progress.v - proof of type soundness
- Subst.v - proof of the substitution lemma for PLLC
- Preservation.v - proof of type preservation, relying on the substitution lemma
- Soundness.v - proof of soundness, relying on progress and preservation
Dependencies
- Coq v8.4. I've tested with 8.4pl5 specifically, on OS X.
Build Instructions
$ git clone --recursive https://github.com/michaelsproul/dblib-linear
$ make
The recursive Git clone just ensures that DbLib gets pulled in.
Stepping Through Interactively
Once you've run make
you should be able to step through any individual file using CoqIDE or
an editor of your choice. You just have to make sure to pass the -R . LLC
option to the Coq
process at some point. For CoqIDE you can pass this flag via the command-line.
$ coqide -R . LLC .
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].