A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
From MaRDI portal
Publication:5019018
DOI10.1017/S0956796820000076OpenAlexW3014596948WikidataQ113857456 ScholiaQ113857456MaRDI QIDQ5019018
James T. E. Chapman, Conor McBride, James McKinna, Guillaume Allais, Robert Atkey
Publication date: 27 December 2021
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2001.11001
Related Items
Semantic analysis of normalisation by evaluation for typed lambda calculus, A well-known representation of monoids and its application to the function ‘vector reverse’, Rensets and renaming-based recursion for syntax with bindings extended version, POPLMark reloaded: Mechanizing proofs by logical relations, A framework for substructural type systems, Variable binding and substitution for (nameless) dummies, A formalized general theory of syntax with bindings: extended version, Rensets and renaming-based recursion for syntax with bindings, A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A new approach to abstract syntax with variable binding
- Data structures and program transformation
- Notions of computation and monads
- Kripke-style models for typed lambda calculus
- Deforestation: Transforming programs to eliminate trees
- Inductive families
- Substitution: A formal methods case study using monads and transformations
- A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
- The locally nameless representation
- Nested abstract syntax in Coq
- Strongly typed term representations in Coq
- Intuitionistic model constructions and normalization proofs
- Coeffects
- Transporting functions across ornaments
- GMeta: A Generic Formal Metatheory Framework for First-Order Representations
- Copatterns
- Tridirectional typechecking
- The Lean Theorem Prover (System Description)
- Data types à la carte
- Initial Algebra Semantics for Cyclic Sharing Structures
- The essence of the <scp>Iterator</scp> pattern
- Dependently Typed Programming in Agda
- A coherence theorem for Martin-Löf's type theory
- de Bruijn notation as a nested datatype
- Shrinking lambda expressions in linear time
- The Zipper
- On bunched typing
- The view from the left
- Derivable Type Classes
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- Categorical reconstruction of a reduction free normalization proof
- POPLMark reloaded: Mechanizing proofs by logical relations
- The gentle art of levitation
- Total parser combinators
- Binders unbound
- Monads need not be endofunctors
- Parametric higher-order abstract syntax for mechanized semantics
- Relative Monads Formalised
- A case study in programming coinductive proofs: Howe’s method
- Automatically Generated Infrastructure for De Bruijn Syntaxes
- Indexed containers
- Idris, a general-purpose dependently typed programming language: Design and implementation
- Bounded Linear Types in a Resource Semiring
- A Core Quantitative Coeffect Calculus
- Applicative programming with effects
- Theorem Proving in Higher Order Logics
- Types for Proofs and Programs
