Denotational semantics as a foundation for cost recurrence extraction for functional languages
From MaRDI portal
Publication:5101922
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
Uses Software
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