Denotational semantics as a foundation for cost recurrence extraction for functional languages
From MaRDI portal
Recommendations
Cites work
- A Coq library for internal verification of running-times
- A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
- Adventures in time and space
- Amortised resource analysis with separation logic
- Amortized resource analysis with polynomial potential. A static inference of polynomial bounds for functional programs
- Analysing the complexity of functional programs: higher-order meets first-order
- Automated higher-order complexity analysis
- Can programming be liberated from the von Neumann style?
- Cost analysis of object-oriented bytecode programs
- Denotational cost semantics for functional languages with inductive types
- Explicit substitutions
- GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and laziness
- scientific article; zbMATH DE number 42735 (Why is no real title available?)
- scientific article; zbMATH DE number 194916 (Why is no real title available?)
- scientific article; zbMATH DE number 2120508 (Why is no real title available?)
- Improvements for free
- Lightweight semiformal time complexity analysis for purely functional data structures
- Linear dependent types and relative completeness
- Mechanical program analysis
- Multivariate amortized resource analysis
- On the inference of resource usage upper and lower bounds
- Parallel cost analysis
- Purely Functional Data Structures
- Relational cost analysis
- Resource bound certification
- Static determination of quantitative resource usage for higher-order programs
- Static prediction of heap space usage for first-order functional programs
- The Category-Theoretic Solution of Recursive Domain Equations
- The semantics of second-order lambda calculus
- Towards automatic resource bound analysis for OCaml
- Two languages for estimating program efficiency
- Type-based cost analysis for lazy functional languages
- Verifying asymptotic time complexity of imperative programs in Isabelle
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
Cited in
(2)
This page was built for publication: Denotational semantics as a foundation for cost recurrence extraction for functional languages
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5101922)
