The following pages link to Explicit substitutions (Q4939690):
Displayed 50 items.
- A prismoid framework for languages with resources (Q654907) (← links)
- Lambda abstraction algebras: representation theorems (Q674002) (← links)
- Semantics of the typed \(\lambda\)-calculus with substitution in a cartesian closed category (Q687575) (← links)
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions (Q714797) (← links)
- An abstract framework for environment machines (Q804281) (← links)
- Simplifying the signature in second-order unification (Q843951) (← 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)
- 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)
- 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)
- Linear Lambda Calculus and Deep Inference (Q3007666) (← links)