A verified framework for higher-order uncurrying optimizations
From MaRDI portal
Publication:968367
DOI10.1007/s10990-010-9050-zzbMath1209.68106OpenAlexW2073733988MaRDI QIDQ968367
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
compiler optimizationfunctional programming languagescompiler verificationmechanized verificationsemantic preservation
Uses Software
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
