Relational cost analysis in a functional-imperative setting
From MaRDI portal
Recommendations
Cites work
- A type theory for incremental computational complexity with control flow changes
- Abstract effects and proof-relevant logical relations
- Amortised resource analysis with separation logic
- An Algorithm for the Machine Calculation of Complex Fourier Series
- Automating induction for solving Horn clauses
- Complexity and resource bound analysis of imperative programs using difference constraints
- Cost recurrences for DML programs
- Denotational cost semantics for functional languages with inductive types
- Higher-order approximate relational refinement types for mechanism design and differential privacy
- Hoare type theory, polymorphism and separation
- scientific article; zbMATH DE number 7204445 (Why is no real title available?)
- Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)
- Lightweight semiformal time complexity analysis for purely functional data structures
- Linear dependent types and relative completeness
- Linear dependent types for differential privacy
- Logical relations for fine-grained concurrency
- Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
- Multivariate amortized resource analysis
- Non-parametric parametricity
- Probabilistic relational verification for cryptographic implementations
- Programming Languages and Systems
- Relational cost analysis
- Simple relational correctness proofs for static analyses and program transformations
- State-dependent representation independence
- Why3 -- where programs meet provers
Cited in
(2)
This page was built for publication: Relational cost analysis in a functional-imperative setting
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5020903)
