Explicit substitutions
From MaRDI portal
Recommendations
Cites work
- Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
- scientific article; zbMATH DE number 3961577 (Why is no real title available?)
- scientific article; zbMATH DE number 3730111 (Why is no real title available?)
- Proof of termination of the rewriting system SUBSET on CCL
Cited in
(only showing first 100 items - show all)- A rewriting logic approach to operational semantics
- Substitution revisited
- A notation for lambda terms. A generalization of environments
- A note on complexity measures for inductive classes in constructive type theory
- Explicit substitution. On the edge of strong normalization
- Unification with extended patterns
- A finite equational axiomatization of the functional algebras for the lambda calculus
- MLOG: A strongly typed confluent functional language with logical variables
- Head linear reduction and pure proof net extraction
- Categorical abstract machines for higher-order typed -calculi
- Label-selective -calculus syntax and confluence
- A useful -notation
- Lambda calculus with explicit recursion
- Computing in unpredictable environments: semantics, reduction strategies, and program transformations
- Revisiting the notion of function
- Theorem proving modulo
- Axiomatisation of substitution
- Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
- Comparing logics for rewriting: Rewriting logic, action calculi and tile logic
- Regular language representations in the constructive type theory of Coq
- Incorporating quotation and evaluation into Church's type theory
- A calculus for reasoning about software composition
- Normalisation for higher-order calculi with explicit substitutions
- Lambda-calculus with director strings
- Comparing and implementing calculi of explicit substitutions with eta-reduction
- Skew confluence and the lambda calculus with letrec
- Higher order unification via explicit substitutions
- Higher-order substitutions
- Pattern matching as cut elimination
- Intersection types for explicit substitutions
- Simply typed lambda calculus with first-class environments
- Point-free substitution
- A lazy desugaring system for evaluating programs with sugars
- Spinal atomic \(\lambda\)-calculus
- The spirit of node replication
- Nominal rewriting
- On explicit substitution with names
- 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
- Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions
- Explicit fusions
- Extensional higher-order paramodulation in Leo-III
- CINNI -- a generic calculus of explicit substitutions and its application to -, - and -calculi
- Explicit environments
- Dependent types and explicit substitutions: A meta-theoretical development
- Cut rules and explicit substitutions
- scientific article; zbMATH DE number 1722651 (Why is no real title available?)
- Strong normalization of substitutions
- Classical by-need
- Incorporating quotation and evaluation into Church's type theory: syntax and semantics
- Certifying term rewriting proofs in ELAN
- Definability and full abstraction
- Local bigraphs and confluence: two conjectures (extended abstract)
- Sub--calculi, classified
- A rewriting logic approach to operational semantics (extended abstract)
- The \(\lambda\)-context calculus
- Linear lambda calculus and deep inference
- Programming inductive proofs. A new approach based on contextual types
- λν, a calculus of explicit substitutions which preserves strong normalisation
- Unification for -calculi without propagation rules
- The Prismoid of Resources
- Term-Generic Logic
- scientific article; zbMATH DE number 4177054 (Why is no real title available?)
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- Mechanized Verification of CPS Transformations
- Why Would You Trust B?
- Inter-deriving Semantic Artifacts for Object-Oriented Programming
- Encoding the Pure Lambda Calculus into Hierarchical Graph Rewriting
- Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
- The Substitution Vanishes
- SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi
- Explicit substitutions calculi with one step eta-reduction decided explicitly
- scientific article; zbMATH DE number 1222417 (Why is no real title available?)
- scientific article; zbMATH DE number 1231543 (Why is no real title available?)
- scientific article; zbMATH DE number 1330136 (Why is no real title available?)
- ON STEPWISE EXPLICIT SUBSTITUTION
- scientific article; zbMATH DE number 1070568 (Why is no real title available?)
- scientific article; zbMATH DE number 1088030 (Why is no real title available?)
- Linear explicit substitutions
- scientific article; zbMATH DE number 1500649 (Why is no real title available?)
- scientific article; zbMATH DE number 1508928 (Why is no real title available?)
- On explicit substitutions and names (extended abstract)
- Substitution, jumps, and algebraic effects
- Term graph rewriting
- Theoretical Pearl Yet yet a counterexample for λ+SP
- Lilac: a functional programming language based on linear logic
- The suspension notation for lambda terms and its use in metalanguage implementations
- Comparing calculi of explicit substitutions with eta-reduction
- Intersection types and computational rules
- Explicit substitutions à la de Bruijn: the local and global way
- scientific article; zbMATH DE number 1424037 (Why is no real title available?)
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
- Rule formats for nominal process calculi
- scientific article; zbMATH DE number 7379288 (Why is no real title available?)
- scientific article; zbMATH DE number 7456059 (Why is no real title available?)
- Strongly-Normalizing Higher-Order Relational Queries
- On confluence for weakly normalizing systems
- Explicit substitutions with de bruijn's levels
- Combinatory reduction systems with explicit substitution that preserve strong normalisation
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)
