1,066 papers · page 42 of 54
Past attempts to relate two well-known models of backtracking computation have met with only limited success. We relate these two models using logical relations. We accommodate higher-order values and infinite computations. We also provide an operational semantics, and we prove i…
It is now 20 years since the Ericsson Computer Science Laboratory (CSLab) was formed, and 20 years since CSLab started performing the programming language experiments that eventually led to the development of the Erlang programming language. For 15 years, Ericsson has conducted e…
Concurrency, as a useful feature of many modern programming languages and systems, is generally hard to reason about. Although existing work has explored the verification of concurrent programs using high-level languages and calculi, the verification of concurrent assembly code r…
All classical ?-terms typable with disjunctive normal forms are shown to share a common computational behavior: they implement a local exception handling mechanism whose exact workings depend on the tautology. Equivalent and more efficient control combinators are described throug…
We present the functional language CDuce, discuss some design issues, and show its adequacy for working with XML documents. Distinctive features of CDuce are a powerful pattern matching, first class functions, overloaded functions, a very rich type system (arrows, sequences, pair…
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 identifiers tha…
We propose a type system MLF that generalizes ML with first-class polymorphism as in System F. Expressions may contain second-order type annotations. Every typable expression admits a principal type, which however depends on type annotations. Principal types capture all other typ…
By allowing the programmer to write code that can generate code at run-time, meta-programming offers a powerful approach to program construction. For instance, meta-programming can often be employed to enhance program efficiency and facilitate the construction of generic programs…
Lazy programs are beautiful, but they are slow because they build many thunks. Simple measurements show that most of these thunks are unnecessary: they are in fact always evaluated, or are always cheap. In this paper we describe Optimistic Evaluation --- an evaluation strategy th…
To improve the quality of type error messages in functional programming languages, we propose four techniques which influence the behaviour of constraint-based type inference processes. These techniques take the form of externally supplied type inference directives, precluding th…
This paper presents a static type system for JAVA Virtual Machine (JVM) code that enforces an access control mechanism similar to the one found, for example, in a JAVA implementation. In addition to verifying type consistency of a given JVM code, the type system statically verifi…
We present the derivation of a space efficient parser combinator library: the constructed parsers do not keep unnecessary references to the input, produce online results and efficiently handle ambiguous grammars. The underlying techniques can be applied in many contexts where tra…
We describe extensions to the Excel spreadsheet that integrate userdefined functions into the spreadsheet grid, rather than treating them as a "bolt-on". Our first objective was to bring the benefits of additional programming language features to a system that is often not recogn…
The shift and reset operators, proposed by Danvy and Filinski, are powerful control primitives for capturing delimited continuations. Delimited continuation is a similar concept as the standard (unlimited) continuation, but it represents part of the rest of the computation, rathe…
Microscopic physics is entirely reversible, yet almost all computation is done using irreversible processes. Adding two numbers together, for example, destroys information, unless one of the numbers is retained. Over the past few years, some advantages of taking reversible comput…
Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent stores. In this paper we combine the two, developing compile-time and run-time se…
Pattern matching mechanisms based on regular expressions feature in a number of recent languages for processing tree-structured data such as XML. A compiler for such a language must address not only the familiar problems of pattern optimization for ML-style algebraic datatypes an…
Generic Haskell is an extension of Haskell that supports the construction of generic programs. During the development of several applications, such as an XML editor and compressor, we encountered a number of limitations with the existing (Classic) Generic Haskell language, as imp…
We give a tutorial and first-principles description of the context semantics of Gonthier, Abadi, and Lévy [5, 4], a computer-science analogue of Girard's geometry of interaction [3]. In the spirit of the invited presentation of Tom Knight (see this Proceedings [7]), the semantics…
We develop an explicit two level system that allows programmers to reason about the behavior of effectful programs. The first level is an ordinary ML-style type system, which confers standard properties on program behavior. The second level is a conservative extension of the firs…