Getting There and Back Again

DOI10.3233/FI-222106MaRDI QIDQ5074057zbMATH OpenFDO

Authors Olivier Danvy

Publication date 6 May 2022

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2203.00145

zbMATH Keywords

continuationsCoq Proof Assistantdefunctionalization and refunctionalizationeta redexeslambda-lifting and lambda-droppinglightweight fusion and lightweight fissionlist processingrecursion patternsymbolic convolutionsTABAThere and Forth Again (TAFA)

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• There and back again
• An exercise in transformational programming: Backtracking and Branch-and- Bound
• Backtrack Programming with SIMULA
• scientific article; zbMATH DE number 598180
• Zippy Tabulations of Recursive Functions

Cites work

• A method for numerical integration on an automatic computer
• Back to direct style
• Definitional interpreters for higher-order programming languages
• Definitional interpreters revisited
• scientific article; zbMATH DE number 3550181 (Why is no real title available?)
• scientific article; zbMATH DE number 194911 (Why is no real title available?)
• scientific article; zbMATH DE number 3285139 (Why is no real title available?)
• scientific article; zbMATH DE number 3342643 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Lambda-dropping: Transforming recursive equations into programs with block structure
• Lightweight fusion by fixed point promotion
• On typing delimited continuations: Three new solutions to the printf problem
• Proceedings of the seventh ACM SIGPLAN international conference on Functional programming
• Refunctionalization at work
• Some remarks on type systems for course-of-value recursion
• State-transition machines for lambda-calculus expressions
• State-transition machines, revisited
• Swapping Arguments and Results of Recursive Functions
• The Mechanical Evaluation of Expressions
• There and back again

Cited in

(4)

• Travelling with Dexter Kozen
• Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant
• Going home through an unknown street
• Along the way back from the brink

Describes a project that uses

Uses Software

• Lantern

This page was built for publication: Getting There and Back Again

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5074057)