Sciweavers

JFP
2008
97views more  JFP 2008»
13 years 9 months ago
HM(X) type inference is CLP(X) solving
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...
Martin Sulzmann, Peter J. Stuckey
JFP
2008
67views more  JFP 2008»
13 years 11 months ago
Efficient execution in an automated reasoning environment
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...
JFP
2008
125views more  JFP 2008»
13 years 11 months ago
Types and trace effects of higher order programs
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...
Christian Skalka, Scott F. Smith, David Van Horn
JFP
2008
85views more  JFP 2008»
13 years 11 months ago
Applicative programming with effects
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...
Conor McBride, Ross Paterson
JFP
2008
109views more  JFP 2008»
13 years 11 months ago
An operational semantics for Scheme
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...
Jacob Matthews, Robert Bruce Findler
JFP
2008
75views more  JFP 2008»
13 years 11 months ago
Exploiting reachability and cardinality in higher-order flow analysis
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...
Matthew Might, Olin Shivers
JFP
2008
72views more  JFP 2008»
13 years 11 months ago
Dynamic rebinding for marshalling and update, via redex-time and destruct-time reduction
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 ...
JFP
2008
61views more  JFP 2008»
13 years 11 months ago
Control reduction theories: the benefit of structural substitution
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 ...
Zena M. Ariola, Hugo Herbelin
JFP
2008
135views more  JFP 2008»
13 years 11 months ago
Hoare type theory, polymorphism and separation
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...