Programs Using Syntax with First-Class Binders

DOI10.1007/978-3-662-54434-1_19zbMath1485.68064OpenAlexW2596094020MaRDI QIDQ2988654

Brigitte Pientka, Francisco Ferreira

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 programminghigher-order abstract syntaxMLprogramming with binders

Mathematics Subject Classification ID

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

Related Items

Rensets and renaming-based recursion for syntax with bindings extended version, A formalized general theory of syntax with bindings: extended version, Rensets and renaming-based recursion for syntax with bindings

Uses Software

• HYBRID
• Haskell
• OCaml
• Twelf
• Freshml
• Delphin
• MiniML

Cites Work

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