Type-and-Scope Safe Programs and Their Proofs - Formalization

Dataset

Description

This dataset comprises a self-contained git repository of the accompanying machine checked proofs/programs from the paper "Type-and-Scope Programs and Their Proofs". The proofs are written in the dependently typed programming language Agda. The dataset also contains the LaTeX source of the paper which is itself a literate Agda file. This dataset is open source software.
Date made available9 Dec 2016
PublisherUniversity of Strathclyde

Cite this

Chapman, J. (Creator), McBride, C. (Creator), Allais, G. (Creator), McKinna, J. (Creator). (9 Dec 2016). Type-and-Scope Safe Programs and Their Proofs - Formalization. University of Strathclyde. type_scope_semantics_master(.zip). 10.15129/f1283dbb-64fd-4d35-aacc-49d3cc0893b8