A verified framework for higher-order uncurrying optimizations
From MaRDI portal
Publication:968367
DOI10.1007/S10990-010-9050-ZzbMATH Open1209.68106OpenAlexW2073733988MaRDI QIDQ968367FDOQ968367
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
Recommendations
compiler optimizationfunctional programming languagescompiler verificationmechanized verificationsemantic preservation
Cites Work
- Theorem Proving in Higher Order Logics
- Combinatory logic. With two sections by William Craig.
- Logical relations and the typed λ-calculus
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Formal verification of translation validators
- The Mechanical Evaluation of Expressions
- Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine
- Programming Languages and Systems
- A call-by-name lambda-calculus machine
- Title not available (Why is that?)
- Explicit substitutions
- Dynamic typing: Syntax and proof theory
- Hybrid type checking
- The categorical abstract machine
- Extraction in Coq: An Overview
- A calculus with polymorphic and polyvariant flow types
- Imperative self-adjusting computation
- Higher-order arity raising
- Making a fast curry: push/enter vs. eval/apply for higher-order languages
- Higher-order unCurrying
Cited In (2)
Uses Software
This page was built for publication: A verified framework for higher-order uncurrying optimizations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q968367)
