The following pages link to Explicit substitutions (Q4939690):
Displayed 50 items.
- 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)
- On generic context lemmas for higher-order calculi with sharing (Q960863) (← links)
- A verified framework for higher-order uncurrying optimizations (Q968367) (← links)
- Inter-deriving semantic artifacts for object-oriented programming (Q980939) (← 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)
- On explicit substitution with names (Q2392486) (← 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)
- Certifying Term Rewriting Proofs in ELAN (Q2841249) (← links)
- Definability and Full Abstraction (Q2864154) (← links)
- Local Bigraphs and Confluence: Two Conjectures (Q2866344) (← links)
- A Rewriting Logic Approach to Operational Semantics (Extended Abstract) (Q2871834) (← links)
- Linear Lambda Calculus and Deep Inference (Q3007666) (← links)
- Programming Inductive Proofs (Q3058448) (← links)
- λν, a calculus of explicit substitutions which preserves strong normalisation (Q3125228) (← links)
- The Prismoid of Resources (Q3182947) (← links)