Reference. A Coq Library For Internal Verification of Running-Times
Cite
Cited by (1)
Polynomial Time and Dependent Types atkey-2024-polynomial
We combine dependent types with linear type systems that soundly and completely capture polynomial time computation. We explore two systems for capturing polynomial time: one system that disallows construction of iterable data, and one, based on the LFPL system of Martin Hofmann, that controls construction via a payment method. Both of these are extended to full dependent types via Quantitative Type Theory, allowing for arbitrary computation in types alongside guaranteed polynomial time computation in terms. We prove the soundness of the systems using a realisability technique due to Dal Lago and Hofmann. Our long-term goal is to combine the extensional reasoning of type theory with intensional reasoning about the resources intrinsically consumed by programs. This paper is a step along this path, which we hope will lead both to practical systems for reasoning about programs’ resource usage, and to theoretical use as a form of synthetic computational complexity theory .
Cites 24 works (2 here)
With notes (2)
Parameterised notions of computation atkey-2009-parameterised
Moggi’s Computational Monads and Power et al .‘s equivalent notion of Freyd category have captured a large range of computational effects present in programming languages. Examples include non-termination, non-determinism, exceptions, continuations, side effects and input/output. We present generalisations of both computational monads and Freyd categories, which we call parameterised monads and parameterised Freyd categories, that also capture computational effects with parameters. Examples of such are composable continuations, side effects where the type of the state varies and input/output where the range of inputs and outputs varies. By considering structured parameterisation also, we extend the range of effects to cover separated side effects and multiple independent streams of I/O. We also present two typed λ-calculi that soundly and completely model our categorical definitions – with and without symmetric monoidal parameterisation – and act as prototypical languages with parameterised effects.
Dependent types in practical programming xi-1999-dependent
External (22)
- Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation (2015)
- Automatic static cost analysis for parallel programs (2015)
- A static cost analysis for a higher-order language (2013)
- Verifying higher-order programs with the dijkstra monad (2013)
- Monads Need Not Be Endofunctors (2010)
- Characteristic formulae for mechanized program verification (2010)
- Introduction to Algorithms (2009)
- SPEED: precise and efficient static estimation of program computational complexity (2009)
- A Hoare Logic for the State Monad (2009)
- A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq (2009)
- Lightweight semiformal time complexity analysis for purely functional data structures (2008)
- Subset coercions in Coq (2006)
- Functors for Proofs and Programs (2004)
- Static prediction of heap space usage for first-order functional programs (2003)
- Denial of service via algorithmic complexity attacks (2003)
- Resource bound certification (2000)
- Recursion and dynamic data-structures in bounded space: towards embedded ML programming (1999)
- Dependently typed data structures (1999)
- Dependent types in practical programming (PhD dissertation) (1999)
- Three algorithms on Braun trees (1997)
- Automatic complexity analysis (1989)
- A logarithmic implementation of flexible arrays (1983)