The following pages link to Explicit substitutions (Q4939690):
Displaying 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)
- Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness (Q730088) (← links)
- N. G. de Bruijn's contribution to the formalization of mathematics (Q740481) (← 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)
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility (Q896904) (← 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)
- Regular language representations in the constructive type theory of Coq (Q1663246) (← links)
- Incorporating quotation and evaluation into Church's type theory (Q1753993) (← 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)
- A lazy desugaring system for evaluating programs with sugars (Q2163178) (← links)
- Spinal atomic \(\lambda\)-calculus (Q2200851) (← links)
- The spirit of node replication (Q2233421) (← links)