Denotational semantics as a foundation for cost recurrence extraction for functional languages

DOI10.1017/S095679682200003XMaRDI QIDQ5101922

Daniel R. Licata, Norman Danner

Publication date: 2 September 2022

Published in: Journal of Functional Programming (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Uses Software

• ACE
• TiML

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• The semantics of second-order lambda calculus
• Cost analysis of object-oriented bytecode programs
• Verifying asymptotic time complexity of imperative programs in Isabelle
• Automated higher-order complexity analysis
• A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
• Type-based cost analysis for lazy functional languages
• A Coq Library for Internal Verification of Running-Times
• Static prediction of heap space usage for first-order functional programs
• GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and laziness
• On the Inference of Resource Usage Upper and Lower Bounds
• Denotational cost semantics for functional languages with inductive types
• Analysing the complexity of functional programs: higher-order meets first-order
• Lightweight semiformal time complexity analysis for purely functional data structures
• Amortised Resource Analysis with Separation Logic
• Amortized Resource Analysis with Polynomial Potential
• The Category-Theoretic Solution of Recursive Domain Equations
• Mechanical program analysis
• Can programming be liberated from the von Neumann style?
• Parallel Cost Analysis
• Purely Functional Data Structures
• Two languages for estimating program efficiency
• Linear Dependent Types and Relative Completeness
• Explicit substitutions
• Resource bound certification
• Static determination of quantitative resource usage for higher-order programs
• Adventures in time and space
• Relational cost analysis
• Towards automatic resource bound analysis for OCaml
• Multivariate amortized resource analysis

This page was built for publication: Denotational semantics as a foundation for cost recurrence extraction for functional languages