916 papers · page 22 of 46
Abstract We report on an experience using the Coq proof assistant to develop a program verification tool with a machine-checked proof of full correctness. The verifier is able to prove memory safety of x86 machine code programs compiled from code that uses algebraic datatypes. Th…
Abstract Concurrent programs require high-level abstractions in order to manage complexity and enable compositional reasoning. In this paper, we introduce a novel concurrency abstraction, dubbed transactional events , which combines first-class synchronous message passing events …
Abstract Ziggurat is a meta-language system that permits programmers to develop Scheme-like macros for languages with nontrivial static semantics, such as C or Java (suitably encoded in an S-expression concrete syntax). Ziggurat permits language designers to construct ‘towers’ of…
Abstract 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 features supporting this method allow the user to install, in a logically sound way, altern…
Abstract This paper develops a new framework for fusion that is designed for eliminating the intermediate data structures involved in the composition of functions that have one accumulating parameter. The new fusion framework comprises two steps: algebraic fusion and its subseque…
Abstract There are two ways to write a program for manipulating tree-structured data such as XML documents: One is to write a tree-processing program focusing on the logical structure of the data and the other is to write a stream-processing program focusing on the physical struc…
The Eleventh ACM SIGPLAN International Conference on Functional Programming (ICFP 2006) took place on September 18–20, 2006 in Portland, Oregon. ICFP 2006 provides a forum for researchers and developers to hear about the latest work on the design, implementation, principles, and …
Abstract This paper presents an operational semantics for the core of Scheme. Our specification improves over the denotational semantics from the Revised 5 Report on Scheme specification in four ways. First, it covers a larger part of the language, specifically eval , quote , dyn…
Abstract In this article, we introduce Applicative functors – an abstract characterisation of an applicative style of effectful programming, weaker than Monads and hence more widespread. Indeed, it is the ubiquity of this programming pattern that drew us to the abstraction. We re…
Abstract We present two complementary improvements for abstract-interpretation-based flow analysis of higher-order languages: (1) abstract garbage collection and (2) abstract counting . Abstract garbage collection is an analog to its concrete counterpart: the analysis determines …
Abstract Jane Street Capital is a successful proprietary trading company that uses OCaml as its primary development language. We have over twenty OCaml programmers and hundreds of thousands of lines of OCaml code. We use OCaml for a wide range of tasks: critical trading systems, …
Abstract We consider the problem of reconciling a dependently typed functional language with imperative features such as mutable higher-order state, pointer aliasing, and nontermination. We propose Hoare type theory (HTT), which incorporates Hoare-style specifications into types,…
Abstract Family polymorphism has been proposed for object-oriented languages as a solution to supporting reusable yet type-safe mutually recursive classes. A key idea of family polymorphism is the notion of families, which are used to group mutually recursive classes. In the orig…
Abstract This paper proves correctness of Nöcker's method of strictness analysis, implemented in the Clean compiler, which is an effective way for strictness analysis in lazy functional languages based on their operational semantics. We improve upon the work Clark, Hankin and Hun…
Abstract 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 guises, for example, when a marshalled value is received from the network, containing ident…
Abstract 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 properties verified are based on the ordered sequence of events that occur during program e…
Abstract 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 program text, which are then solved by the domain-specific constraint solver X. The solver has to …
Abstract This paper describes a technique for assembling both data types and functions from isolated individual components. We also explore how the same technology can be used to combine free monads and, as a result, structure Haskell's monolithic IO monad.
Abstract Higher-order abstract syntax is a simple technique for implementing languages with functional programming. Object variables and binders are implemented by variables and binders in the host language. By using this technique, one can avoid implementing common and tricky ro…
Abstract We present a compositional programme logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters, return values, content of references and parts of data structures. The p…