A type- and scope-safe universe of syntaxes with binding: their semantics and proofs

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

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

• GitHub

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