Sciweavers

ASWEC
2004
IEEE
13 years 8 months ago
Obstacles to a Totally Functional Programming Style
"Totally Functional Programming" (TFP) advocates the complete replacement of symbolic representations for data by functions. TFP is motivated by observations from practi...
Paul A. Bailes, Colin J. M. Kemp
ASIAN
2003
Springer
109views Algorithms» more  ASIAN 2003»
13 years 9 months ago
Deaccumulation - Improving Provability
Several induction theorem provers were developed to verify functional programs mechanically. Unfortunately, automated verification usually fails for functions with accumulating ar...
Jürgen Giesl, Armin Kühnemann, Janis Voi...
PPDP
2009
Springer
13 years 11 months ago
Model-checking higher-order functions
We propose a novel type-based model checking algorithm for higher-order recursion schemes. As shown by Kobayashi, verification problems of higher-order functional programs can ea...
Naoki Kobayashi
TPHOL
2009
IEEE
13 years 11 months ago
A Hoare Logic for the State Monad
Abstract. This pearl examines how to verify functional programs written using the state monad. It uses Coq’s Program framework to provide strong specifications for the standard ...
Wouter Swierstra
ESOP
2010
Springer
13 years 11 months ago
Amortized Resource Analysis with Polynomial Potential
In 2003, Hofmann and Jost introduced a type system that uses a potential-based amortized analysis to infer bounds on the resource consumption of (first-order) functional programs....
Jan Hoffmann 0002, Martin Hofmann
ESOP
2010
Springer
14 years 1 months ago
Amortized Resource Analysis with Polynomial Potential - A Static Inference of Polynomial Bounds for Functional Programs
In 2003, Hofmann and Jost introduced a type system that uses a potential-based amortized analysis to infer bounds on the resource consumption of (first-order) functional programs. ...
Jan Hoffmann and Martin Hofmann