GitHub - cmcl/msci: MSci project: Development of a formalisation of "Propositions as Sessions"

cmcl / msci Public

Notifications You must be signed in to change notification settings
Fork 0
Star 2

MSci project: Development of a formalisation of "Propositions as Sessions"

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 246 Commits
Coq Developments		Coq Developments
Paper reviews		Paper reviews
paper		paper
proposal		proposal
.gitignore		.gitignore
MsciProjectIdeasEmail		MsciProjectIdeasEmail
README		README
SimonGay		SimonGay
SimonPaperQs		SimonPaperQs

Repository files navigation

Formalisation of Session-based Lambda Calculus Type Systems
------------------------------------------------------------

For the Coq development see: ./Coq Developments/msci/

The Makefile should compile both the top-level proof scripts and the UPenn
Metatheory library.

Note the .dir_locals.el file (currently) has a hardcoded directory path for
looking for the Coq files. This file is loaded by Proof General when
interacting with the Coq system. You do not require to change it if you do not
intend to run the development.