Pages that link to "Item:Q2949209"
From MaRDI portal
The following pages link to A compiled implementation of strong reduction (Q2949209):
Displayed 41 items.
- Proof-carrying code from certified abstract interpretation and fixpoint compression (Q860842) (← links)
- Choices in representation and reduction strategies for lambda terms in intensional contexts (Q861365) (← links)
- Refunctionalization at work (Q923881) (← links)
- Proof synthesis and reflection for linear arithmetic (Q945055) (← links)
- A computer-verified monadic functional implementation of the integral (Q987984) (← links)
- A verified ODE solver and the Lorenz attractor (Q1663218) (← links)
- Lambda-calculus with director strings (Q1778107) (← links)
- The \textsc{MetaCoq} project (Q2209542) (← links)
- The spirit of node replication (Q2233421) (← links)
- (In)efficiency and reasonable cost models (Q2333310) (← links)
- Strongly reducing variants of the Krivine abstract machine (Q2464720) (← links)
- Mechanized semantics for the clight subset of the C language (Q2655325) (← links)
- Extensible and Efficient Automation Through Reflective Tactics (Q2802496) (← links)
- The Useful MAM, a Reasonable Implementation of the Strong $$\lambda $$ -Calculus (Q2820681) (← links)
- A Certified Reduction Strategy for Homological Image Processing (Q2946732) (← links)
- Structural recursion with locally scoped names (Q3016213) (← links)
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq (Q3100210) (← links)
- Open Call-by-Value (Q3179293) (← links)
- A Compiled Implementation of Normalization by Evaluation (Q3543648) (← links)
- First-Class Type Classes (Q3543665) (← links)
- Abstract λ-Calculus Machines (Q3599179) (← links)
- A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance (Q3637183) (← links)
- Typed Applicative Structures and Normalization by Evaluation for System F ω (Q3644739) (← links)
- (Q4957791) (← links)
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus (Q4972064) (← links)
- Fold–unfold lemmas for reasoning about recursive programs using the Coq proof assistant (Q5051990) (← links)
- The Negligible and Yet Subtle Cost of Pattern Matching (Q5056004) (← links)
- (Q5076060) (← links)
- A Fresh Look at the λ-Calculus (Q5089000) (← links)
- (Q5089007) (← links)
- (Q5111306) (← links)
- New Developments in Environment Machines (Q5170161) (← links)
- Computer Certified Efficient Exact Reals in Coq (Q5200110) (← links)
- Denotational aspects of untyped normalization by evaluation (Q5313717) (← links)
- Mtac: A monad for typed tactic programming in Coq (Q5371944) (← links)
- Constructive Mathematics and Functional Programming (Abstract) (Q5458392) (← links)
- (Q5856420) (← links)
- Primitive Floats in Coq (Q5875413) (← links)
- Enabling floating-point arithmetic in the Coq proof assistant (Q6053846) (← links)
- A strong call-by-need calculus (Q6135746) (← links)
- Node Replication: Theory And Practice (Q6192004) (← links)