Explicit substitutions
From MaRDI portal
Publication:4939690
DOI10.1017/S0956796800000186zbMath0941.68542OpenAlexW4236324644MaRDI QIDQ4939690
Martín Abadi, Jean-Jacques Levy, Luca Cardelli, Pierre-Louis Curien
Publication date: 9 February 2000
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0956796800000186
Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Combinatory logic and lambda calculus (03B40)
Related Items
Termination of term rewriting by interpretation ⋮ Denotational semantics as a foundation for cost recurrence extraction for functional languages ⋮ Closure under alpha-conversion ⋮ Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Algebraic interpretation of lambda calculus with resources ⋮ Spiritus asper versus lambda: on the nature of functional abstraction ⋮ Towards a constructive simplicial model of Univalent Foundations ⋮ A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi ⋮ Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Explicit substitutions for \(\pi\)-congruences ⋮ A typed context calculus ⋮ Proof-term synthesis on dependent-type systems via explicit substitutions ⋮ The Role of Structural Reasoning in the Genesis of Graph Theory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Normalization by Evaluation for Typed Weak lambda-Reduction ⋮ Unnamed Item ⋮ THE SOUNDNESS OF EXPLICIT SUBSTITUTION WITH NAMELESS VARIABLES ⋮ Substitution inconsistencies in Transparent Intensional Logic ⋮ Strong normalization of substitutions ⋮ Full abstraction for lambda calculus with resources and convergence testing ⋮ Strongly-Normalizing Higher-Order Relational Queries ⋮ Pattern matching as cut elimination ⋮ Unnamed Item ⋮ Intersection types for explicit substitutions ⋮ Head linear reduction and pure proof net extraction ⋮ Nominal rewriting ⋮ LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners ⋮ Simplifying the signature in second-order unification ⋮ On confluence for weakly normalizing systems ⋮ Explicit substitutions with de bruijn's levels ⋮ Combinatory reduction systems with explicit substitution that preserve strong normalisation ⋮ Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract) ⋮ The Negligible and Yet Subtle Cost of Pattern Matching ⋮ Simply typed lambda calculus with first-class environments ⋮ Decomposing typed lambda calculus into a couple of categorical programming languages ⋮ Categorical abstract machines for higher-order typed \(\lambda\)-calculi ⋮ Unification for $$\lambda $$ -calculi Without Propagation Rules ⋮ Label-selective \(\lambda\)-calculus syntax and confluence ⋮ The Prismoid of Resources ⋮ Term-Generic Logic ⋮ Explicit substitutions and higher-order syntax ⋮ The Rule of Existential Generalisation and Explicit Substitution ⋮ On explicit substitution with names ⋮ Choices in representation and reduction strategies for lambda terms in intensional contexts ⋮ A useful \(\lambda\)-notation ⋮ A lazy desugaring system for evaluating programs with sugars ⋮ Regular language representations in the constructive type theory of Coq ⋮ Unnamed Item ⋮ On explicit substitutions and names (extended abstract) ⋮ Resource operators for \(\lambda\)-calculus ⋮ A syntactic correspondence between context-sensitive calculi and abstract machines ⋮ Lambda calculus with explicit recursion ⋮ A \(\rho\)-calculus of explicit constraint application ⋮ Extensional higher-order paramodulation in Leo-III ⋮ A notation for lambda terms. A generalization of environments ⋮ Computing in unpredictable environments: semantics, reduction strategies, and program transformations ⋮ Mechanized Verification of CPS Transformations ⋮ Why Would You Trust B? ⋮ Revisiting the notion of function ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Inter-deriving Semantic Artifacts for Object-Oriented Programming ⋮ Spinal atomic \(\lambda\)-calculus ⋮ Unnamed Item ⋮ Encoding the Pure Lambda Calculus into Hierarchical Graph Rewriting ⋮ Unnamed Item ⋮ A prismoid framework for languages with resources ⋮ Theorem proving modulo ⋮ Unnamed Item ⋮ Axiomatisation of substitution ⋮ The spirit of node replication ⋮ Explaining the lazy Krivine machine using explicit substitution and addresses ⋮ Strongly reducing variants of the Krivine abstract machine ⋮ On the correctness of the Krivine machine ⋮ Linear Lambda Calculus and Deep Inference ⋮ Lambda abstraction algebras: representation theorems ⋮ Term graph rewriting ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ Semantics of the typed \(\lambda\)-calculus with substitution in a cartesian closed category ⋮ The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations ⋮ Comparing Calculi of Explicit Substitutions with Eta-reduction ⋮ On generic context lemmas for higher-order calculi with sharing ⋮ Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions ⋮ A verified framework for higher-order uncurrying optimizations ⋮ Intersection Types and Computational Rules ⋮ Explicit Substitutions à la de Bruijn ⋮ A calculus for reasoning about software composition ⋮ Normalisation for higher-order calculi with explicit substitutions ⋮ Inter-deriving semantic artifacts for object-oriented programming ⋮ PNL to HOL: from the logic of nominal sets to the logic of higher-order functions ⋮ Lambda-calculus with director strings ⋮ Comparing and implementing calculi of explicit substitutions with eta-reduction ⋮ Programming Inductive Proofs ⋮ Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness ⋮ Classical By-Need ⋮ Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions ⋮ N. G. de Bruijn's contribution to the formalization of mathematics ⋮ A rewriting logic approach to operational semantics ⋮ Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ⋮ A Fresh Look at the λ-Calculus ⋮ A note on complexity measures for inductive classes in constructive type theory ⋮ Explicit substitution. On the edge of strong normalization ⋮ Unification with extended patterns ⋮ SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi ★ ⋮ A finite equational axiomatization of the functional algebras for the lambda calculus ⋮ Certifying Term Rewriting Proofs in ELAN ⋮ Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions ⋮ Explicit fusions ⋮ λν, a calculus of explicit substitutions which preserves strong normalisation ⋮ Skew confluence and the lambda calculus with letrec ⋮ Higher order unification via explicit substitutions ⋮ Higher-order substitutions ⋮ Definability and Full Abstraction ⋮ Local Bigraphs and Confluence: Two Conjectures ⋮ An abstract framework for environment machines ⋮ Theoretical Pearl Yet yet a counterexample for λ+SP ⋮ MLOG: A strongly typed confluent functional language with logical variables ⋮ Lilac: a functional programming language based on linear logic ⋮ A Rewriting Logic Approach to Operational Semantics (Extended Abstract) ⋮ Comparing logics for rewriting: Rewriting logic, action calculi and tile logic
Cites Work
