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...
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...
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 ...
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...
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,...
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...
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...
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...
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...