A universe of binding and computation

DOI10.1145/1596550.1596571zbMATH Open1302.68050OpenAlexW1989866935MaRDI QIDQ2936809FDOQ2936809

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

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

zbMATH Keywords

dependent typesvariable binding

Mathematics Subject Classification ID

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

Cited In (10)

• From signatures to monads in \textsf{UniMath}
• Denotational semantics with nominal Scott domains
• A formalized general theory of syntax with bindings: extended version
• Structural recursion with locally scoped names
• POPLMark reloaded: mechanizing proofs by logical relations
• Computational universes
• Programming with binders and indexed data-types
• 2-Dimensional Directed Type Theory
• Title not available (Why is that?)
• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs

Uses Software

• Freshml
• Agda

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)