A universe of binding and computation

DOI10.1145/1596550.1596571MaRDI QIDQ2936809zbMATH OpenOpenAlexFDO

Authors Daniel R. Licata, Robert Harper

Publication date 6 January 2015

Published in Proceedings of the 14th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.150.4264

zbMATH Keywords

dependent typesvariable binding

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Recommendations

• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
• Programming with binders and indexed data-types
• Binders unbound
• From signatures to monads in \textsf{UniMath}
• A fresh look at programming with names and binders

Cited in

(12)

• A formalized general theory of syntax with bindings: extended version
• From signatures to monads in \textsf{UniMath}
• Computational universes
• Programming with binders and indexed data-types
• Structural recursion with locally scoped names
• scientific article; zbMATH DE number 1149906 (Why is no real title available?)
• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
• POPLMark reloaded: mechanizing proofs by logical relations
• Denotational semantics with nominal Scott domains
• 2-Dimensional Directed Type Theory
• Formalisation in constructive type theory of Barendregt's variable convention for generic structures with binders
• A monadic formalization of ML5

Describes a project that uses

Uses Software

• Agda
• FreshML

This page was built for publication: A universe of binding and computation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2936809)