Programs Using Syntax with First-Class Binders
From MaRDI portal
Publication:2988654
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
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
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