Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism

DOI10.1017/S0956796807006557zbMath1128.68021OpenAlexW2096280839MaRDI QIDQ5437034

Geoffrey Washburn, Stephanie Weirich

Publication date: 18 January 2008

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796807006557

zbMATH Keywords

iteration operatorsfusion laws

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, Programs Using Syntax with First-Class Binders, Syntax for Free: Representing Syntax with Binding Using Parametricity, Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages

Uses Software

• Haskell
• Twelf

Cites Work

• Unnamed Item
• Polytypic values possess polykinded types
• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• A generalization of short-cut fusion and its correctness proof
• A judgmental reconstruction of modal logic
• Recursion over objects of functional type
• Meta-programming with names and necessity
• A modal analysis of staged computation
• A completeness theorem in modal logic
• Practical type inference for arbitrary-rank types
• Type-safe run-time polytypic programming
• A proof theory for generic judgments
• A formulation of the simple theory of types
• Primitive recursion for higher-order abstract syntax
• A hybrid approach to online and offline partial evaluation