The following pages link to Explicit substitutions (Q4939690):
Displayed 50 items.
- Lambda abstraction algebras: representation theorems (Q674002) (← links)
- Semantics of the typed \(\lambda\)-calculus with substitution in a cartesian closed category (Q687575) (← links)
- An abstract framework for environment machines (Q804281) (← links)
- Explicit substitutions and higher-order syntax (Q853744) (← links)
- Choices in representation and reduction strategies for lambda terms in intensional contexts (Q861365) (← links)
- Resource operators for \(\lambda\)-calculus (Q876041) (← links)
- A syntactic correspondence between context-sensitive calculi and abstract machines (Q879356) (← links)
- A \(\rho\)-calculus of explicit constraint application (Q880989) (← links)
- A rewriting logic approach to operational semantics (Q1012130) (← links)
- A notation for lambda terms. A generalization of environments (Q1129257) (← links)
- A note on complexity measures for inductive classes in constructive type theory (Q1271558) (← links)
- Explicit substitution. On the edge of strong normalization (Q1274458) (← links)
- Unification with extended patterns (Q1274966) (← links)
- A finite equational axiomatization of the functional algebras for the lambda calculus (Q1283777) (← links)
- MLOG: A strongly typed confluent functional language with logical variables (Q1314424) (← links)
- Head linear reduction and pure proof net extraction (Q1342250) (← links)
- Categorical abstract machines for higher-order typed \(\lambda\)-calculi (Q1349667) (← links)
- Label-selective \(\lambda\)-calculus syntax and confluence (Q1350342) (← links)
- A useful \(\lambda\)-notation (Q1365680) (← links)
- Lambda calculus with explicit recursion (Q1383145) (← links)
- Computing in unpredictable environments: semantics, reduction strategies, and program transformations (Q1389440) (← links)
- Revisiting the notion of function (Q1394989) (← links)
- Theorem proving modulo (Q1431339) (← links)
- Axiomatisation of substitution (Q1433380) (← links)
- Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions (Q1575247) (← links)
- Comparing logics for rewriting: Rewriting logic, action calculi and tile logic (Q1608920) (← links)
- A calculus for reasoning about software composition (Q1770365) (← links)
- Normalisation for higher-order calculi with explicit substitutions (Q1770414) (← links)
- Lambda-calculus with director strings (Q1778107) (← links)
- Comparing and implementing calculi of explicit substitutions with eta-reduction (Q1779307) (← links)
- Skew confluence and the lambda calculus with letrec (Q1849854) (← links)
- Higher order unification via explicit substitutions (Q1854337) (← links)
- Higher-order substitutions (Q1854398) (← links)
- Pattern matching as cut elimination (Q1882898) (← links)
- Intersection types for explicit substitutions (Q1887145) (← links)
- Simply typed lambda calculus with first-class environments (Q1894315) (← links)
- Nominal rewriting (Q2373703) (← links)
- Explaining the lazy Krivine machine using explicit substitution and addresses (Q2464715) (← links)
- Strongly reducing variants of the Krivine abstract machine (Q2464720) (← links)
- On the correctness of the Krivine machine (Q2464724) (← links)
- Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions (Q2480966) (← links)
- Explicit fusions (Q2566040) (← links)
- (Q2703692) (← links)
- λν, a calculus of explicit substitutions which preserves strong normalisation (Q3125228) (← links)
- Mechanized Verification of CPS Transformations (Q3498467) (← links)
- Why Would You Trust B? (Q3498474) (← links)
- Inter-deriving Semantic Artifacts for Object-Oriented Programming (Q3511441) (← links)
- Encoding the Pure Lambda Calculus into Hierarchical Graph Rewriting (Q3522032) (← links)
- Strong cut-elimination in sequent calculus using Klop's <i>ι</i>-translation and perpetual reductions (Q3617369) (← links)
- (Q4222859) (← links)