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