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



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

Research Output

  • 1 Conference contribution book

Type-and-scope safe programs and their proofs

Allais, G., Chapman, J., McBride, C. & McKinna, J., 16 Jan 2017, CPP 2017 : Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. Bertot, Y. & Vafeiadis, V. (eds.). New York, 13 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Open Access
  • 15 Citations (Scopus)
    80 Downloads (Pure)


  • 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