Code for: "A type and scope safe universe of syntaxes with binding: their semantics and proofs"

Guillaume Allais (Creator)
Bob Atkey (Creator)
James Chapman (Creator)
Conor McBride (Creator)
James McKinna (Creator)

Dataset

Description

Replication Package for Article: "A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs".

Code and documentation available from the ACM Digital Library and GitHub

Date made available	23 Aug 2018
Publisher	Association for Computing Machinery (ACM)

Contact

[email protected]

DOI
10.1145/3235048

Access Dataset

The software is also available from github

1 Conference Contribution

A type and scope safe universe of syntaxes with binding: their semantics and proofs
Allais, G., Atkey, R., Chapman, J., McBride, C. & McKinna, J., 23 Sept 2018, In: Proceedings of the ACM on Programming Languages (PACMPL). 2, ICFP, p. 1-30 30 p., 90.
Research output: Contribution to journal › Conference Contribution › peer-review

Open Access
File
23 Citations (Scopus)

120 Downloads (Pure)

1 Finished

Homotopy Type Theory: Programming and Verification
Ghani, N. (Principal Investigator) & McBride, C. (Co-investigator)
EPSRC (Engineering and Physical Sciences Research Council)
1/04/15 → 30/09/19
Project: Research

Cite this