Sciweavers

ICFP
2008
ACM
15 years 24 days ago
A type-preserving compiler in Haskell
There has been a lot of interest of late for programming languages that incorporate features from dependent type systems and proof assistants in order to capture in the types impo...
Louis-Julien Guillemette, Stefan Monnier
ICFP
2008
ACM
15 years 24 days ago
Functional translation of a calculus of capabilities
Reasoning about imperative programs requires the ability to track aliasing and ownership properties. We present a type system that provides this ability, by using regions, capabil...
Arthur Charguéraud, François Pottier
ICFP
2008
ACM
15 years 24 days ago
Mixin' up the ML module system
ML modules provide hierarchical namespace management, as well as fine-grained control over the propagation of type information, but they do not allow modules to be broken up into ...
Derek Dreyer, Andreas Rossberg
ICFP
2008
ACM
15 years 24 days ago
HMF: simple type inference for first-class polymorphism
HMF is a conservative extension of Hindley-Milner type inference with first-class polymorphism. In contrast to other proposals, HML uses regular System F types and has a simple ty...
Daan Leijen
ICFP
2008
ACM
15 years 24 days ago
Typed iterators for XML
XML transformations are very sensitive to types: XML types describe the tags and attributes of XML elements as well as the number, kind, and order of their sub-elements. Therefore,...
Giuseppe Castagna, Kim Nguyen
ICFP
2008
ACM
15 years 24 days ago
Write it recursively: a generic framework for optimal path queries
Optimal path queries are queries to obtain an optimal path specified by a given criterion of optimality. There have been many studies to give efficient algorithms for classes of o...
Akimasa Morihata, Kiminori Matsuzaki, Masato Takei...
ICFP
2008
ACM
15 years 24 days ago
Deciding kCFA is complete for EXPTIME
David Van Horn, Harry G. Mairson
ICFP
2008
ACM
15 years 24 days ago
Ynot: dependent types for imperative programs
We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. C...
Aleksandar Nanevski, Greg Morrisett, Avraham Shinn...
ICFP
2008
ACM
15 years 24 days ago
The power of Pi
This paper exhibits the power of programming with dependent types by dint of embedding three domain-specific languages: Cryptol, a language for cryptographic protocols; a small da...
Nicolas Oury, Wouter Swierstra
ICFP
2008
ACM
15 years 24 days ago
Typed closure conversion preserves observational equivalence
Language-based security relies on the assumption that all potential attacks are bound by the rules of the language in question. When programs are compiled into a different languag...
Amal Ahmed, Matthias Blume