Explicit substitutions
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 3961577 (Why is no real title available?)
- scientific article; zbMATH DE number 3730111 (Why is no real title available?)
- Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
- Proof of termination of the rewriting system SUBSET on CCL
Cited in
(only showing first 100 items - show all)- Syntax monads for the working formal metatheorist
- scientific article; zbMATH DE number 1508928 (Why is no real title available?)
- Combinatory reduction systems with explicit substitution that preserve strong normalisation
- The Substitution Vanishes
- Substitution, jumps, and algebraic effects
- Lambda-calculus with director strings
- scientific article; zbMATH DE number 7559273 (Why is no real title available?)
- scientific article; zbMATH DE number 7204428 (Why is no real title available?)
- On explicit substitutions and names (extended abstract)
- Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
- Denotational semantics as a foundation for cost recurrence extraction for functional languages
- Computing in unpredictable environments: semantics, reduction strategies, and program transformations
- Explicit substitutions à la de Bruijn: the local and global way
- On the correctness of the Krivine machine
- Full substitutability
- The role of structural reasoning in the genesis of graph theory
- Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
- Revisiting the notion of function
- A flexible framework for visualisation of computational properties of general explicit substitutions calculi
- Inter-deriving semantic artifacts for object-oriented programming
- Strong normalization of substitutions
- Explicit environments
- A verified framework for higher-order uncurrying optimizations
- A lambda calculus with letrecs and barriers
- A rewriting logic approach to operational semantics
- Categorical abstract machines for higher-order typed \(\lambda\)-calculi
- Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
- Semantics of the typed \(\lambda\)-calculus with substitution in a cartesian closed category
- Linear explicit substitutions
- Encoding the Pure Lambda Calculus into Hierarchical Graph Rewriting
- Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
- Explicit fusions
- Simplifying the signature in second-order unification
- scientific article; zbMATH DE number 1722651 (Why is no real title available?)
- Explicit substitutions with de bruijn's levels
- Substitution revisited
- A note on complexity measures for inductive classes in constructive type theory
- The Negligible and Yet Subtle Cost of Pattern Matching
- Full abstraction for lambda calculus with resources and convergence testing
- Extensional higher-order paramodulation in Leo-III
- Explicit substitutions and higher-order syntax
- The spirit of node replication
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
- A \(\rho\)-calculus of explicit constraint application
- scientific article; zbMATH DE number 7456059 (Why is no real title available?)
- Axiomatisation of substitution
- Unification with extended patterns
- A typed context calculus
- Classical by-need
- Explaining the lazy Krivine machine using explicit substitution and addresses
- Incorporating quotation and evaluation into Church's type theory
- On the computability of relations on \(\lambda \)-terms and Rice's theorem -- the case of the expansion problem for explicit substitutions
- scientific article; zbMATH DE number 1424037 (Why is no real title available?)
- Sub-\(\lambda\)-calculi, classified
- Mechanized Verification of CPS Transformations
- Choices in representation and reduction strategies for lambda terms in intensional contexts
- A finite equational axiomatization of the functional algebras for the lambda calculus
- Simply typed lambda calculus with first-class environments
- Local bigraphs and confluence: two conjectures (extended abstract)
- Algebraic interpretation of lambda calculus with resources
- Unification for \(\lambda\)-calculi without propagation rules
- Spiritus asper versus lambda: on the nature of functional abstraction
- Incorporating quotation and evaluation into Church's type theory: syntax and semantics
- A syntactic correspondence between context-sensitive calculi and abstract machines
- scientific article; zbMATH DE number 1231543 (Why is no real title available?)
- Substitution inconsistencies in transparent intensional logic
- Why Would You Trust B?
- λν, a calculus of explicit substitutions which preserves strong normalisation
- A notation for lambda terms. A generalization of environments
- Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness
- Term-Generic Logic
- The Prismoid of Resources
- The soundness of explicit substitution with nameless variables
- A useful \(\lambda\)-notation
- Higher order unification via explicit substitutions
- Higher-order substitutions
- Lambda calculus with explicit recursion
- An extended type system with lambda-typed lambda-expressions
- N. G. de Bruijn's contribution to the formalization of mathematics
- Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
- A Fresh Look at the λ-Calculus
- Normalisation for higher-order calculi with explicit substitutions
- Comparing logics for rewriting: Rewriting logic, action calculi and tile logic
- Eight rules for implication elimination
- Comments on the contributions
- Head linear reduction and pure proof net extraction
- Extended addressing machines for PCF, with explicit substitutions
- Rule formats for nominal process calculi
- Linear lambda calculus and deep inference
- Explicit substitution. On the edge of strong normalization
- Regular language representations in the constructive type theory of Coq
- MLOG: A strongly typed confluent functional language with logical variables
- scientific article; zbMATH DE number 7204440 (Why is no real title available?)
- Definability and full abstraction
- Point-free substitution
- A lazy desugaring system for evaluating programs with sugars
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
- Normalization by Evaluation for Typed Weak lambda-Reduction
- Explicit substitutions for \(\pi\)-congruences
This page was built for publication: Explicit substitutions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4939690)
