| |
In The Handbook of Logic in Computer Science, Vol. 5 (October 2000)
Abstract
ionb 2 B [x 2 A]([x]b) 2 (x 2 A)BWe will write repeated abstractions as [x 1 ; x 2 ; : : : ; xn ]b and also excludethe outermost parentheses when there is no risk of confusion.How do we know that this rule is correct, i.e. how do we know that [x]bis a function of the type (x 2 A)B? By the semantics of function types,we must know that when we apply [x]b of type (x 2 A)B on ...
|
| |
Journal of Functional Programming, Vol. 8 (1998), pp. 23-60
Abstract
The process of writing large parallel programs is complicated by the need to specify both the parallel behaviour of the program and the algorithm that is to be used to compute its result. This paper introduces evaluation strategies, lazy higher-order functions that control the parallel evaluation of non-strict functional languages. Using evaluation strategies, it is possible to achieve a clean separation between algorithmic and behavioural code. The result is enhanced clarity and shorter parallel programs. Evaluation strategies are a very general ...
|
| |
|
| |
|
| |
posted to programming testing types
by namin
to the group Lambda the Ultimate
on 2008-08-08 02:52:32
Abstract
Parameterized unit tests extend the current industry practice of using closed unit tests defined as parameterless methods. Parameterized unit tests separate two concerns: 1) They specify the external behavior of the involved methods for all possible test arguments. 2) Test cases can be re-obtained as traditional closed unit tests by instantiating the parameterized unit tests. Symbolic execution and constraint solving can be used to automatically choose a minimal set of inputs that exercise a parameterized unit test with respect to possible ...
|
| |
|
| |
(9 May 2008)
Abstract
We argue that the language of Zermelo Fraenkel set theory with definitions and partial functions provides the most promising bedrock semantics for communicating and sharing mathematical knowledge. We then describe a syntactic sugaring of that language that provides a way of writing remarkably readable assertions without straying far from the set-theoretic semantics. We illustrate with some examples of formalized textbook definitions from elementary set theory and point-set topology. We also present statistics concerning the complexity of these definitions, under various complexity measures. ...
|
| |
|
| |
|
| |
(2008)
Abstract
This is the year 2008 and ML-style exceptions are everywhere. Most modern languages, whether academic or industrial, feature some variant of this mechanism. Languages such as Java even have a degree of out-of-the-box static coverage-checking for such exceptions, which is currently not available for ML languages, at least not without resorting to external tools. In this document, we demonstrate a design principle and a tiny library for managing errors in a functional manner, with static coverage-checking, automatically-inferred, structurally typed and hierarchical exceptional ...
|
| |
|
| |
Abstract
JavaScript is a popular language for client-side web scripting. It has a dubious reputation among programmers for two reasons. First, many JavaScript programs are written against a rapidly evolving API whose implementations are sometimes contradictory and idiosyncratic. Second, the language is only weakly typed and comes virtually without development tools. The present work is a first ...
|
| |
|
| |
|
| |
|
| |
Abstract
Virtual machines (VMs) enable the distribution of programs in an architecture-neutral format, which can easily be interpreted or compiled. A long-running question in the design of VMs is whether a stack architecture or register architecture can be implemented more efficiently with an interpreter. We extend existing work on comparing virtual stack and virtual register architectures in three ways. First, our translation from stack to register code and optimization are much more sophisticated. The result is that we eliminate an average of ...
|
| |
posted to interpreter optimization
by pedagand
to the group Lambda the Ultimate
on 2008-07-06 09:30:31
Abstract
Inline-threaded interpretation is a recent technique that improves performance by eliminating dispatch overhead within basic blocks for interpreters written in C [11]. The dynamic class loading, lazy class initialization, and multi-threading features of Java reduce the effiectiveness of a straight-forward implementation of this technique within Java interpreters. In this paper, we introduce preparation sequences, a new technique that solves the particular challenge of effiectively inline-threading Java. We have implemented our technique in the SableVM Java virtual machine, and our experimental results ...
|
| |
In VEE '07: Proceedings of the 3rd international conference on Virtual execution environments (2007), pp. 83-93, doi:10.1145/1254810.1254823
posted to interpreter optimization
by pedagand
to the group Lambda the Ultimate
on 2008-07-06 09:28:08
|
| |
|
| |
In CGO '05: Proceedings of the international symposium on Code generation and optimization (2005), pp. 15-26, doi:10.1109/cgo.2005.14
|
| |
posted to interpreter optimization
by pedagand
to the group Lambda the Ultimate
on 2008-07-06 09:23:53
|
| |
|
| |
|
| |
(2005)
Abstract
This is a slightly odd paper that explains why I am still as fascinated by the combination of functional programming and hardware design as I have ever been. It includes some looking back over my own research and that of others, and contains 60 references. It explains what kinds of research I am doing now, and why, and also presents some neat new results about parallel prefix circuits. It ends by posing lots of hard questions that we need to answer ...
|
| |
|
| |
|
| |
Abstract
. We present two mutual encodings, respectively of the Calculus of Inductive Constructions in Zermelo-Fraenkel set theory and the opposite way. More precisely, we actually construct two families of encodings, relating the number of universes in the type theory with the number of inaccessible cardinals in the set theory. The main result is that both hierarchies of logical formalisms interleave w.r.t. expressive power and thus are essentially equivalent. Both encodings are quite elementary: type... ...
|
| |
In Formal Description of Programming Concepts (1991), pp. 431-507
Abstract
There exists an identifiable programming style based on the widespread use of type information handled through mechanical typechecking techniques. ...
|
| |
Information and Computation, Vol. 115, No. 1. (1994), pp. 38-94
Abstract
We present a new approach to proving type soundness for Hindley/Milner-style polymorphic type systems. The keys to our approach are (1) an adaptation of subject reduction theorems from combinatory logic to programming languages, and (2) the use of rewriting techniques for the specification of the language semantics. The approach easily extends from polymorphic functional languages to imperative languages that provide references, exceptions, continuations, and similar features. We illustrate the ... ...
|
| |
(2002)
posted to ai programming theory
by namin
to the group Lambda the Ultimate
on 2008-05-20 21:42:04
|
| |
|
| |
In Program Design Calculi: Proceedings of the 1992 Marktoberdorf International Summer School (1993)
Abstract
. The use of monads to structure functional programs is described. Monads provide a convenient framework for simulating effects found in other languages, such as global state, exception handling, output, or non-determinism. Three case studies are looked at in detail: how monads ease the modification of a simple evaluator; how monads act as the basis of a datatype of arrays subject to in-place update; and how monads can be used to build parsers. 1 Introduction Shall I be pure or impure? ...
|
| |
In POPL '97: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (1997), pp. 316-331, doi:10.1145/263699.263744
Abstract
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references. ...
|
| |
SIGPLAN Not. In ICFP '02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, Vol. 37, No. 9. (September 2002), pp. 133-144, doi:10.1145/581478.581492
Abstract
Monads are a useful abstraction of computation, as they model diverse computational effects such as stateful computations, exceptions and I/O in a uniform manner. Their potential to provide both a modular semantics and a modular programming style was soon recognised. However, in general, monads proved difficult to compose and so research focused on special mechanisms for their composition such as distributive monads and monad transformers.We present a new approach to this problem which is general in that nearly all monads compose, ...
|
| |
|
| |
J. Mach. Learn. Res., Vol. 7 (2006), pp. 429-454
posted to homepage synthesis
by pedagand
to the group Lambda the Ultimate
on 2008-05-11 11:53:36
|
| |
Abstract
Few programming languages have a mathematically rigorous definition or metatheory—in part because they are perceived as too large and complex to work with. This paper demonstrates the feasibility of such undertakings: we formalize a substantial portion of the semantics of Objective Caml’s core language (which had not previously been given a formal semantics), and we develop a mechanized type soundness proof in HOL. We also develop an executable version of the operational semantics, verify that it coincides with our semantic definition, ...
|
| |
Abstract
Garbage collection offers numerous software engineering advantages, but interacts poorly with virtual memory managers. Existing garbage collectors require far more pages than the application's working set and touch pages without regard to which ones are in memory, especially during full-heap garbage collection. The resulting paging can cause throughput to plummet and pause times to spike up to seconds or even minutes. We present a garbage collector that avoids paging. This bookmarking collector ... ...
|
| |
Abstract
Garbage collection yields numerous software engineering benefits, but its quantitative impact on performance remains elusive. One can measure the cost of conservative garbage collection relative to explicit memory management in C/C++ programs by linking in an appropriate collector. This kind of direct comparison is not possible for languages designed for garbage collection (e.g., Java), because programs in these languages naturally do not contain calls to free. Thus, the actual gap between the... ...
|
| |
|
| |
In PEPM '08: Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation (2008), pp. 147-157, doi:10.1145/1328408.1328430
|
| |
In OOPSLA '06: Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications (2006), pp. 21-36, doi:10.1145/1167473.1167476
|
| |
(2002)
Abstract
The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces , a lambda-calculus with recursion, inductive types, subtyping and bounded quanti cation. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm... ...
|
| |
(17 Mar 2008)
Abstract
A fully-automated algorithm is developed able to show that evaluation of a given untyped lambda-expression will terminate under CBV (call-by-value). The “size-change principle” from first-order programs is extended to arbitrary untyped lambda-expressions in two steps. The first step suffices to show CBV termination of a single, stand-alone lambda-expression. The second suffices to show CBV termination of any member of a regular set of lambda-expressions, defined by a tree grammar. (A simple example is a minimum function, when applied to arbitrary Church numerals.) The algorithm is sound and proven ...
|
| |
Abstract
Machine-checked proofs of properties of programming languages have become acritical need, both for increased confidence in large and complex designsand as a foundation for technologies such as proof-carrying code. However, constructing these proofs remains a black art, involving many choices in the formulation of definitions and theorems that make a huge cumulative difference in the difficulty of carrying out large formal developments. There presentation and manipulation of terms with variable binding is a key issue. We propose a novel style for ...
|
| |
Abstract
When scripts in untyped languages grow into large programs, maintaining them becomes difficult. A lack of types in typical scripting languages means that programmers must (re)discover critical pieces of design information every time they wish to change a program. This analysis step both slows down the maintenance process and may even introduce mistakes due to the violation of undiscovered invariants. This paper presents Typed Scheme, an explicitly typed extension of an untyped scripting language. Its type system is based on the ...
|
| |
In ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming (1998), pp. 251-260, doi:10.1145/289423.289452
|
| |
(1995)
posted to homepage system-f system-r
by pedagand
to the group Lambda the Ultimate
on 2008-05-11 11:27:11
Abstract
System R is an extension of system F that formalizes Reynolds' notion of relational parametricity. In this paper we describe a semantics for system R. As a first step, we give a careful and general reconstruction of the per model of system F of Bainbridge et al., presenting it as a categorical model in the sense of Seely. Then we interpret system R in this model. LIENS, CNRS - D'epartement de Math'ematiques et Informatique de l'Ecole Normale Sup'erieure and Dipartimento di Matematica,... ...
|
| |
Abstract
We present a certified compiler from the simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler and the terms of its several intermediate languages are given dependent types that guarantee that only well-typed programs are representable. Thus, type preservation for each compiler pass follows without any significant "proofs" of the usual kind. Semantics preservation is proved based on denotational ...
|
| |
In ICFP '07: Proceedings of the 2007 ACM SIGPLAN international conference on Functional programming (2007), pp. 85-96, doi:10.1145/1291151.1291166
|
Search
