A compiled implementation of strong reduction

DOI10.1145/581478.581501zbMath1322.68053OpenAlexW2168254994MaRDI 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

zbMATH Keywords

abstract machinecalculus of constructionsvirtual machinenormalization by evaluationCoqstrong reductionbeta-equivalence

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Fold–unfold lemmas for reasoning about recursive programs using the Coq proof assistant ⋮ The Negligible and Yet Subtle Cost of Pattern Matching ⋮ Open Call-by-Value ⋮ Unnamed Item ⋮ Denotational aspects of untyped normalization by evaluation ⋮ Proof-carrying code from certified abstract interpretation and fixpoint compression ⋮ Choices in representation and reduction strategies for lambda terms in intensional contexts ⋮ Mechanized semantics for the clight subset of the C language ⋮ A verified ODE solver and the Lorenz attractor ⋮ Unnamed Item ⋮ A Certified Reduction Strategy for Homological Image Processing ⋮ Enabling floating-point arithmetic in the Coq proof assistant ⋮ A strong call-by-need calculus ⋮ Node Replication: Theory And Practice ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ The \textsc{MetaCoq} project ⋮ Refunctionalization at work ⋮ A Compiled Implementation of Normalization by Evaluation ⋮ First-Class Type Classes ⋮ Primitive Floats in Coq ⋮ The spirit of node replication ⋮ Strongly reducing variants of the Krivine abstract machine ⋮ Proof synthesis and reflection for linear arithmetic ⋮ Structural recursion with locally scoped names ⋮ New Developments in Environment Machines ⋮ Unnamed Item ⋮ Lambda-calculus with director strings ⋮ Abstract λ-Calculus Machines ⋮ Unnamed Item ⋮ A computer-verified monadic functional implementation of the integral ⋮ Computer Certified Efficient Exact Reals in Coq ⋮ Extensible and Efficient Automation Through Reflective Tactics ⋮ Constructive Mathematics and Functional Programming (Abstract) ⋮ Unnamed Item ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ⋮ The Useful MAM, a Reasonable Implementation of the Strong $$\lambda $$ -Calculus ⋮ A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance ⋮ A Fresh Look at the λ-Calculus ⋮ Typed Applicative Structures and Normalization by Evaluation for System F ω ⋮ Modular SMT Proofs for Fast Reflexive Checking Inside Coq ⋮ (In)efficiency and reasonable cost models

Uses Software

• Coq
• OCaml