Explicit substitutions and higher-order syntax

DOI10.1007/S10990-006-8748-4zbMATH Open1105.68021OpenAlexW2108760508MaRDI QIDQ853744FDOQ853744

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

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

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)

Cites Work

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

Cited In (20)

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

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)