The following pages link to Explicit substitutions (Q4939690):
Displayed 50 items.
- Programming Inductive Proofs (Q3058448) (← links)
- λν, a calculus of explicit substitutions which preserves strong normalisation (Q3125228) (← links)
- Unification for $$\lambda $$ -calculi Without Propagation Rules (Q3179400) (← links)
- The Prismoid of Resources (Q3182947) (← links)
- Term-Generic Logic (Q3184738) (← links)
- LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners (Q3453128) (← 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)
- SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi ★ (Q3647258) (← links)
- (Q4222859) (← links)
- On explicit substitutions and names (extended abstract) (Q4571957) (← links)
- Term graph rewriting (Q4645801) (← links)
- <i>Theoretical Pearl</i> Yet yet a counterexample for λ+SP (Q4764268) (← links)
- Lilac: a functional programming language based on linear logic (Q4764609) (← links)
- The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations (Q4916200) (← links)
- Comparing Calculi of Explicit Substitutions with Eta-reduction (Q4916203) (← links)
- Intersection Types and Computational Rules (Q4924527) (← links)
- Explicit Substitutions à la de Bruijn (Q4924548) (← links)
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus (Q4972064) (← links)
- (Q4972733) (← links)
- (Q5009703) (← links)
- (Q5021229) (← links)
- Strongly-Normalizing Higher-Order Relational Queries (Q5043580) (← links)
- On confluence for weakly normalizing systems (Q5055761) (← links)
- Explicit substitutions with de bruijn's levels (Q5055838) (← links)
- Combinatory reduction systems with explicit substitution that preserve strong normalisation (Q5055859) (← links)
- Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract) (Q5055860) (← links)
- The Negligible and Yet Subtle Cost of Pattern Matching (Q5056004) (← links)
- Decomposing typed lambda calculus into a couple of categorical programming languages (Q5057475) (← links)
- The Rule of Existential Generalisation and Explicit Substitution (Q5066098) (← links)
- A Fresh Look at the λ-Calculus (Q5089000) (← links)
- (Q5089006) (← links)
- (Q5089035) (← links)
- Normalization by Evaluation for Typed Weak lambda-Reduction (Q5091147) (← links)
- Strong normalization of substitutions (Q5096832) (← links)
- Denotational semantics as a foundation for cost recurrence extraction for functional languages (Q5101922) (← links)
- POPLMark reloaded: Mechanizing proofs by logical relations (Q5110924) (← links)
- (Q5111304) (← links)
- (Q5111317) (← links)
- (Q5140267) (← links)
- A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi (Q5179010) (← links)
- The Role of Structural Reasoning in the Genesis of Graph Theory (Q5208125) (← links)
- THE SOUNDNESS OF EXPLICIT SUBSTITUTION WITH NAMELESS VARIABLES (Q5248982) (← links)
- Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus (Q5747746) (← links)
- Substitution inconsistencies in Transparent Intensional Logic (Q5862004) (← links)
- Full abstraction for lambda calculus with resources and convergence testing (Q5878917) (← links)
- Termination of term rewriting by interpretation (Q5881183) (← links)