Getting There and Back Again

DOI10.3233/FI-222106MaRDI QIDQ5074057

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

continuationslist processingCoq Proof Assistantdefunctionalization and refunctionalizationeta redexeslambda-lifting and lambda-droppinglightweight fusion and lightweight fissionrecursion patternsymbolic convolutionsTABAThere and Forth Again (TAFA)

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items (1)

Fold–unfold lemmas for reasoning about recursive programs using the Coq proof assistant

Uses Software

• Lantern

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A method for numerical integration on an automatic computer
• Refunctionalization at work
• On typing delimited continuations: Three new solutions to the printf problem
• Definitional interpreters revisited
• Definitional interpreters for higher-order programming languages
• Back to direct style
• Lambda-dropping: Transforming recursive equations into programs with block structure
• State-transition machines for lambda-calculus expressions
• State-transition machines, revisited
• Lightweight fusion by fixed point promotion
• Swapping Arguments and Results of Recursive Functions
• Some Remarks on Type Systems for Course-of-value Recursion
• The Mechanical Evaluation of Expressions
• Proceedings of the seventh ACM SIGPLAN international conference on Functional programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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