The HM(X) system is a generalization of the Hindley/Milner system parameterized in the constraint domain X. Type inference is performed by generating constraints out of the progra...
We describe a method that permits the user of a mechanized mathematical logic to write elegant logical definitions while allowing sound and efficient execution. In particular, the...
David A. Greve, Matt Kaufmann, Panagiotis Manolios...
This paper shows how type effect systems can be combined with model-checking techniques to produce powerful, automatically verifiable program logics for higher order programs. The...
In this paper, we introduce Applicative functors--an abstract characterisation of an applicative style of effectful programming, weaker than Monads and hence more widespread. it i...
This paper presents an operational semantics for the core of Scheme. Our specification improves over the denotational semantics from the Revised5 Report on Scheme specification in...
t two complementary improvements for abstract-interpretation-based flow analysis r-order languages: (1) abstract garbage collection and (2) abstract counting.1,2 garbage collecti...
Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various...
Peter Sewell, Gareth Stoyle, Michael Hicks, Gavin ...
The historical design of the call-by-value theory of control relies on the reification of evaluation contexts as regular functions and on the use of ordinary term application for ...
We consider the problem of reconciling a dependently typed functional language with imperative features such as mutable higher-order state, pointer aliasing, and non-termination. ...
Aleksandar Nanevski, J. Gregory Morrisett, Lars Bi...