Formal Reasoning About Programs

Coq plugin embedding elpi

being the lecture materials and exercises for the 2017/18 session of CS410 Advanced Functional Programming at the University of Strathclyde

Formalization of Linear Logic

Bartosz Milewski's 'Category Theory for Programmers' unofficial PDF and LaTeX source

SubExponential Linear Logic Framework for reasoning about sequent calculus systems