A verified framework for higher-order uncurrying optimizations

DOI10.1007/s10990-010-9050-zzbMath1209.68106OpenAlexW2073733988MaRDI QIDQ968367

Zaynah Dargaye, Xavier Leroy

Publication date: 5 May 2010

Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10990-010-9050-z

zbMATH Keywords

compiler optimizationfunctional programming languagescompiler verificationmechanized verificationsemantic preservation

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Uses Software

• Coq
• PoplMark

Cites Work

• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Combinatory logic. With two sections by William Craig.
• The categorical abstract machine
• Dynamic typing: Syntax and proof theory
• A call-by-name lambda-calculus machine
• Formal verification of translation validators
• Imperative self-adjusting computation
• Extraction in Coq: An Overview
• Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine
• Logical relations and the typed λ-calculus
• A calculus with polymorphic and polyvariant flow types
• Explicit substitutions
• Higher-order arity raising
• Hybrid type checking
• Theorem Proving in Higher Order Logics
• Making a fast curry: push/enter vs. eval/apply for higher-order languages
• The Mechanical Evaluation of Expressions
• Programming Languages and Systems
• Higher-order unCurrying

This page was built for publication: A verified framework for higher-order uncurrying optimizations