A compiled implementation of strong reduction
From MaRDI portal
Publication:2949209
DOI10.1145/581478.581501zbMath1322.68053MaRDI QIDQ2949209
Benjamin Grégoire, Xavier Leroy
Publication date: 7 October 2015
Published in: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01499941/file/strong-reduction.pdf
abstract machine; calculus of constructions; virtual machine; normalization by evaluation; Coq; strong reduction; beta-equivalence
68N18: Functional programming and lambda calculus
68Q60: Specification and verification (program logics, model checking, etc.)
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, 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, New Developments in Environment Machines, Computer Certified Efficient Exact Reals in Coq, A Fresh Look at the λ-Calculus, Denotational aspects of untyped normalization by evaluation, Mtac: A monad for typed tactic programming in Coq, Constructive Mathematics and Functional Programming (Abstract), Unnamed Item, Primitive Floats in Coq, Enabling floating-point arithmetic in the Coq proof assistant, A strong call-by-need calculus, Node Replication: Theory And Practice, 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, 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 $$\lambda $$ -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 ω
Uses Software
