29 citations · 80 across the 13 of their papers we have counts for
14 papers
Type-Based Analysis of Logarithmic Amortised Complexity
Martin Hofmann, Lorenz Leutgeb, Georg Moser +2
We introduce a novel amortised resource analysis couched in a type-and-effect system. Our analysis is formulated in terms of the physicist's method of amortised analysis, and is po…
Analysis of Logarithmic Amortised Complexity
Martin Hofmann, Georg Moser
We introduce a novel amortised resource analysis based on a potential-based type system. This type system gives rise to logarithmic and polynomial bounds on the runtime complexity…
Linear Tree Constraints
Sabine Bauer, Martin Hofmann
Linear tree constraints were introduced by Hofmann and Rodriguez in the context of amortized resource analysis for object oriented programs. More precisely, they gave a reduction f…
Enforcing Programming Guidelines with Region Types and Effects
Serdar Erbatur, Martin Hofmann, Eugen Zalinescu
We present in this paper a new type and effect system for Java which can be used to ensure adherence to guidelines for secure web programming. The system is based on the region and…
Proof-Relevant Logical Relations for Name Generation
Nick Benton, Martin Hofmann, Vivek Nigam
Pitts and Stark's -calculus is a paradigmatic total language for studying the problem of contextual equivalence in higher-order languages with name generation. Models for the $ν…
An implementation of Deflate in Coq
Christoph-Simon Senjak, Martin Hofmann
The widely-used compression format "Deflate" is defined in RFC 1951 and is based on prefix-free codings and backreferences. There are unclear points about the way these codings are…