A fresh look at programming with names and binders

DOI10.1145/1863543.1863575zbMath1323.68082OpenAlexW2097249860MaRDI QIDQ5176942

Nicolas Pouillard, François Pottier

Publication date: 5 March 2015

Published in: Proceedings of the 15th 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.154.603

zbMATH Keywords

higher-order abstract syntaxbindersnamesmeta-programmingname abstraction

Mathematics Subject Classification ID

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

Related Items (8)

A unified treatment of syntax with binders ⋮ Refined Environment Classifiers ⋮ HOCore in Coq ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Romeo: A system for more flexible binding-safe programming ⋮ Reasoning about multi-stage programs ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ Structural recursion with locally scoped names

Uses Software

• Freshml
• Agda

This page was built for publication: A fresh look at programming with names and binders