Programs using syntax with first-class binders

DOI10.1007/978-3-662-54434-1_19MaRDI QIDQ2988654zbMATH OpenOpenAlexFDO

Authors Francisco Ferreira, Brigitte Pientka

Publication date 19 May 2017

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

Full work available at URL https://doi.org/10.1007/978-3-662-54434-1_19

zbMATH Keywords

functional programmingMLhigher-order abstract syntaxprogramming with binders

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18)

Recommendations

• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Functional programming with higher-order abstract syntax and explicit substitutions
• FreshML: programming with binders made simple
• First-class contexts in ML
• Programming type-safe transformations using higher-order abstract syntax

Cites work

• A framework for defining logics
• A judgmental reconstruction of modal logic
• A modal analysis of staged computation
• A two-level logic approach to reasoning about computations
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism
• Contextual modal type theory
• FreshML: programming with binders made simple
• Guarded recursive datatype constructors
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Inductive beluga: programming proofs
• Nominal logic, a first order theory of names and binding
• Optimizing higher-order pattern unification.
• Parametric higher-order abstract syntax for mechanized semantics
• Programming with binders and indexed data-types
• Romeo: a system for more flexible binding-safe programming
• Strongly typed term representations in Coq

Cited in

(4)

• Rensets and renaming-based recursion for syntax with bindings
• Using circular programs for higher-order syntax (functional pearl)
• A formalized general theory of syntax with bindings: extended version
• Rensets and renaming-based recursion for syntax with bindings extended version

Describes a project that uses

Uses Software

• MiniML
• Delphin
• FreshML
• Twelf
• OCaml
• Haskell
• HYBRID

This page was built for publication: Programs using syntax with first-class binders

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