A compiled implementation of strong reduction
From MaRDI portal
Recommendations
- Strong reduction of combinatory calculus with streams
- Reduction strategies for declarative programming
- Modified strong reduction in combinatory logic
- scientific article; zbMATH DE number 890353
- A direct proof of the confluence of combinatory strong reduction
- Reducing weak to strong bisimilarity in CCP
- Strong and weak reducibility of algorithmic problems
Cited in
(48)- The useful MAM, a reasonable implementation of the strong -calculus
- Lambda-calculus with director strings
- scientific article; zbMATH DE number 7204429 (Why is no real title available?)
- The \textsc{MetaCoq} project
- Genericity through stratification
- (In)efficiency and reasonable cost models
- scientific article; zbMATH DE number 7526055 (Why is no real title available?)
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
- A certified reduction strategy for homological image processing
- The Negligible and Yet Subtle Cost of Pattern Matching
- The spirit of node replication
- Sub-core solutions of the problem of strong implementation
- Proof-carrying code from certified abstract interpretation and fixpoint compression
- Choices in representation and reduction strategies for lambda terms in intensional contexts
- Fast, verified computation for HOL ITPs
- Primitive Floats in Coq
- Refunctionalization at work
- Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant
- Strong call-by-value and multi types
- New developments in environment machines
- Enabling floating-point arithmetic in the Coq proof assistant
- Proof synthesis and reflection for linear arithmetic
- Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
- A Fresh Look at the λ-Calculus
- Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
- Computer Certified Efficient Exact Reals in Coq
- Deriving an abstract machine for strong call by need
- Open call-by-value
- Type directed partial evaluation for level-1 shift and reset
- A formal proof of the irrationality of \(\zeta(3)\)
- A verified ODE solver and the Lorenz attractor
- Modular SMT proofs for fast reflexive checking inside Coq
- Node Replication: Theory And Practice
- First-Class Type Classes
- Mtac: a monad for typed tactic programming in Coq
- A fresh inductive approach to useful call-by-value
- Strongly reducing variants of the Krivine abstract machine
- Structural recursion with locally scoped names
- Denotational aspects of untyped normalization by evaluation
- A Compiled Implementation of Normalization by Evaluation
- Constructive Mathematics and Functional Programming (Abstract)
- A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
- Mechanized semantics for the clight subset of the C language
- A computer-verified monadic functional implementation of the integral
- Abstract λ-Calculus Machines
- Extensible and efficient automation through reflective tactics
- Typed Applicative Structures and Normalization by Evaluation for System F ω
- A lambda term representation inspired by linear ordered logic
This page was built for publication: A compiled implementation of strong reduction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2949209)
