Relational cost analysis in a functional-imperative setting
From MaRDI portal
Publication:5020903
DOI10.1017/S0956796821000071OpenAlexW3210018541MaRDI QIDQ5020903
Weihao Qu, Deepak Garg, Marco Gaboardi
Publication date: 7 January 2022
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1812.04090
Uses Software
Cites Work
- Unnamed Item
- Automating induction for solving Horn clauses
- Complexity and resource bound analysis of imperative programs using difference constraints
- Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)
- Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
- Logical relations for fine-grained concurrency
- Linear dependent types for differential privacy
- Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
- Denotational cost semantics for functional languages with inductive types
- A type theory for incremental computational complexity with control flow changes
- Lightweight semiformal time complexity analysis for purely functional data structures
- Simple relational correctness proofs for static analyses and program transformations
- Hoare type theory, polymorphism and separation
- Amortised Resource Analysis with Separation Logic
- Linear Dependent Types and Relative Completeness
- Non-parametric parametricity
- Cost recurrences for DML programs
- State-dependent representation independence
- Why3 — Where Programs Meet Provers
- An Algorithm for the Machine Calculation of Complex Fourier Series
- Relational cost analysis
- Probabilistic relational verification for cryptographic implementations
- Abstract effects and proof-relevant logical relations
- Multivariate amortized resource analysis
- Programming Languages and Systems
This page was built for publication: Relational cost analysis in a functional-imperative setting
