Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming

DOI10.1007/978-3-642-00590-9_4zbMath1234.68057OpenAlexW1645062691MaRDI QIDQ3617690

Matthew R. Lakin, Andrew M. Pitts

Publication date: 31 March 2009

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-00590-9_4

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (3)

Encoding abstract syntax without fresh names ⋮ Equivariant unification ⋮ αCheck: A mechanized metatheory model checker

This page was built for publication: Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming