Explicit substitutions and higher-order syntax

DOI10.1007/S10990-006-8748-4MaRDI QIDQ853744zbMATH OpenOpenAlexFDO

Authors Neil Ghani, Tarmo Uustalu, Makoto Hamana

Publication date 17 November 2006

Published in Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10990-006-8748-4

zbMATH Keywords

AlgebrasVariable bindingAbstract syntaxExplicit substitutionsMonads

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• Higher-order substitutions
• A Theory of Explicit Substitutions with Safe and Full Composition
• Functional programming with higher-order abstract syntax and explicit substitutions
• Explicit substitutions
• Substitution in non-wellfounded syntax with variable binding

Cites work

• scientific article; zbMATH DE number 3928328 (Why is no real title available?)
• scientific article; zbMATH DE number 1086712 (Why is no real title available?)
• scientific article; zbMATH DE number 1952947 (Why is no real title available?)
• scientific article; zbMATH DE number 2086588 (Why is no real title available?)
• scientific article; zbMATH DE number 1424053 (Why is no real title available?)
• A presentation of topoi as algebraic relative to categories or graphs
• An abstract framework for environment machines
• Composing monads using coproducts
• Dualising initial algebras
• Explicit substitutions
• Explicit substitutions and higher-order syntax
• Free iterative theories: a coalgebraic view
• Generalised folds for nested datatypes
• Infinite trees and completely iterative theories: A coalgebraic view
• Iteration and coiteration schemes for higher-order and nested datatypes
• On iteratable endofunctors
• On rational monads and free iterative theories
• Parametric corecursion
• Substitution in non-wellfounded syntax with variable binding
• de Bruijn notation as a nested datatype

Cited in

(20)

• Modules over monads and initial semantics
• scientific article; zbMATH DE number 1497799 (Why is no real title available?)
• Structured handling of scoped effects
• Functional programming with higher-order abstract syntax and explicit substitutions
• Theoretical Computer Science
• scientific article; zbMATH DE number 1759453 (Why is no real title available?)
• Programming Languages and Systems
• scientific article; zbMATH DE number 7559272 (Why is no real title available?)
• CINNI -- a generic calculus of explicit substitutions and its application to \(\lambda\)-, \(\sigma\)- and \(\pi\)-calculi
• Coproducts of Ideal Monads
• scientific article; zbMATH DE number 7379288 (Why is no real title available?)
• scientific article; zbMATH DE number 1070568 (Why is no real title available?)
• High-level signatures and initial semantics
• Recursion principles for syntax with bindings and substitution
• Substitution in non-wellfounded syntax with variable binding
• Substitution in non-wellfounded syntax with variable binding
• Explicit substitutions and higher-order syntax
• Higher-order substitutions
• Initial Algebra Semantics for Cyclic Sharing Structures
• scientific article; zbMATH DE number 1508928 (Why is no real title available?)

Describes a project that uses

Uses Software

• Haskell

This page was built for publication: Explicit substitutions and higher-order syntax

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