Abstract

Concurrent ML (CML) is a high-level message-passing language that supports the construction of first-class synchronous abstractions called events. This mechanism has proven quite effective over the years and has been incorporated in a number of other languages. While CML provides a concurrent programming model, its implementation has always been limited to uniprocessors. This limitation is exploited in the implementation of the synchronization protocol that underlies the event mechanism, but with the advent of cheap parallel processing on the desktop (and laptop), ...

Note (first note only)

• Concert Reading Group: 05/20/2010

Abstract

In 1972 J.-Y. Girard showed that the Burali-Forti paradox can be formalised in the type system U. In 1991 Th. Coquand formalised another paradox in U–. The corresponding proof terms (that have no normal form) are large. We present a shorter term of type in the Pure Type System U– and analyse its reduction behaviour. The idea is to construct a universe U and two functions such that a certain equality holds. Using this equality, we prove and disprove that ...

Note (first note only)

• Concert Reading Group: 01/07/2010

Abstract

ML modules are a powerful language mechanism for decomposing programs into reusable components. Unfortunately, they also have a reputation for being "complex" and requiring fancy type theory that is mostly opaque to non-experts. While this reputation is certainly understandable, given the many non-standard methodologies that have been developed in the process of studying modules, we aim here to demonstrate that it is undeserved. To do so, we give a very simple elaboration semantics for a full-featured, higher-order ML-like module language. Our ...

Note (first note only)

• Concert Reading Group: 11/17/2009

Abstract

We introduce a first-order dynamic logic for reasoning about systems with discrete and continuous state transitions, and we present a sequent calculus for this logic. As a uniform model, our logic supports hybrid programs with discrete and differential actions. For handling real arithmetic during proofs, we lift quantifier elimination to dynamic logic. To obtain a modular combination, we use side deductions for verifying interacting dynamics. With this, our logic supports deductive verification of hybrid systems with symbolic parameters and first-order definable ...

Note (first note only)

• Concert Reading Group: 10/27/2009

Abstract

The paper describes an abstract interpretation technique based on lazy functional programming, and applies it to the proof of Conway’s Lost Cosmological Theorem, a combinatorial proposition analogous to the four color theorem or Kepler’s conjecture, which essentially states that a certain predicate holds of all lists of integers from 1 to 4. The technique makes use of the semantics of Haskell in the following way: evaluating a predicate on a partial lazy list to True proves that the predicate would evaluate ...

Note (first note only)

• Concert Reading Group: 12/15/2009

Abstract

In 1985 Luca Cardelli and Peter Wegner, my advisor, published an ACM Computing Surveys paper called "On understanding types, data abstraction, and polymorphism". Their work kicked off a flood of research on semantics and type theory for object-oriented programming, which continues to this day. Despite 25 years of research, there is still widespread confusion about the two forms of data abstraction, abstract data types and objects . This essay attempts to explain the differences and also why the ...

Note (first note only)

• Concert Reading Group: 12/01/2009

Abstract

We present an extension to Standard ML, called SMLSC, to support separate compilation. The system gives meaning to individual program fragments, called units. Units may depend on one another in a way specified by the programmer. A dependency may be mediated by an interface (the type of a unit); if so, the units can be compiled separately. Otherwise, they must be compiled in sequence. We also propose a methodology for programming in SMLSC that reflects code development practice and avoids syntactic ...

Note (first note only)

• Concert Reading Group: 11/05/2009

Abstract

Solving large, irregular graph problems efficiently is challenging. Current software systems and commodity multiprocessors do not support fine-grained, irregular parallelism well. We present XWS, the X10 work stealing framework, an open-source runtime for the parallel programming language X10 and a library to be used directly by application writers. XWS extends the Cilk work-stealing framework with several features necessary to efficiently implement graph algorithms, viz., support for improperly nested procedures, global termination detection, and phased computation. We also present a strategy to ...

Abstract

We present the spine calculus S[->]multimap&top as an efficient representation for the linear lambda-calculus lambda[->]multimap&top which includes unrestricted functions ([->]) linear functions (multimap) additive pairing (&) and additive unit (top). S[->]multimap&top enhances the representation of Church's simply typed lambda-calculus by enforcing extensionality and by incorporating linear constructs. This approach permits procedures such as unification to retain the efficient head access that characterizes first-order term languages without the overhead of performing eta-conversions at run time. Applications lie in proof search, logic programming, ...

Abstract

We present a system of refinement types for LF in the style of recent formulations where only canonical forms are well-typed. Both the usual LF rules and the rules for type refinements are bidirectional, leading to a straightforward proof of decidability of type-checking even in the presence of intersection types. Because we insist on canonical forms, structural rules for subtyping can now be derived rather than being assumed as primitive. We illustrate the expressive power of our ...

Abstract

We study two partial type inference methods for a language combining subtyping and impredicative polymorphism. Both methods are local in the sense that missing annotations are recovered using only information from adjacent nodes in the syntax tree, without long-distance constraints such as unification variables. One method infers type arguments in polymorphic applications using a local constraint solver. The other infers annotations on bound variables in function abstractions by propagating type constraints downward from enclosing application nodes. We motivate our design choices ...

Abstract

We derive a control-flow analysis that approximates the interprocedural control-flow of both function calls and returns in the presence of first-class functions and tail-call optimization. In addition to an abstract environment, our analysis computes for each expression an abstract control stack, effectively approximating where function calls return across optimized tail calls. The analysis is systematically calculated by abstract interpretation of the stack-based CaEK abstract machine of Flanagan et al. using a series of Galois connections. Abstract interpretation provides a unifying setting ...

Abstract

Polymorphic regular types are tree-like datatypes generated by polynomial type expressions over a set of free variables and closed under least fixed point. The `equality types' of Core ML can be expressed in this form. Given such a type expression T with x free, this paper shows a way to represent the one-hole contexts for elements of x within elements of T , together with an operation which will plug an element of x into the hole of such a context. ...

Abstract

This paper explores a new point in the design space of functional programming: functional programming with dependently-typed higher-order data structures described in the logical framework LF. This allows us to program with proofs as higher-order data. We present a decidable bidirectional type system that distinguishes between dependently-typed data and computations. To support reasoning about open data, our foundation makes contexts explicit. This provides us with a concise characterization of open data, which is crucial to elegantly describe proofs. In addition, we ...

Note (first note only)

• Concert Reading Group: 10/20/2009

Abstract

An abstract is not available. ...

Note (first note only)

• Classic Papers: 09/28/2009 (Luke Zarko)

Abstract

This paper suggests that input and output are basic primitives of programming and that parallel composition of communicating sequential processes is a fundamental program structuring method. When combined with a development of Dijkstra's guarded command, these concepts are surprisingly versatile. Their use is illustrated by sample solutions of a variety of a familiar programming exercises. ...

Note (first note only)

• Classic Papers: 10/05/2009 (Michael Ashley-Rollman)

Abstract

Compilers for high-level languages are generally constructed to give the complete translation of the programs into machine language. As machines merely juggle bit patterns, the concepts of the original language may be lost or at least obscured during this passage. The purpose of a mathematical semantics is to give a correct and meaningful correspondence between programs and mathematical entities in a way that is entirely independent of an implementation. This plan is illustrated in a very elementary way in the introduction. ...

Note (first note only)

• Classic Papers: 10/14/2009 (Rob Simmons)

Abstract

This paper reports on the development and formal verification (proof of semantic preservation) of CompCert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of critical software and its formal verification: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable ...

Note (first note only)

• Concert Reading Group: 10/13/2009

Abstract

Automatic differentiation (AD) is a precise, efficient, and convenient method for computing derivatives of functions. Its forward-mode implementation can be quite simple even when extended to compute all of the higher-order derivatives as well. The higher-dimensional case has also been tackled, though with extra complexity. This paper develops an implementation of higher-dimensional, higher-order, forward-mode AD in the extremely general and elegant setting of calculus on manifolds and derives that implementation from a simple and precise specification. In order to ...

Note (first note only)

• Concert Reading Group: 10/06/2009

Abstract

There is a mismatch between meta and object levels in many calculi, like the sequent calculus and natural deduction. The mismatch has undesirable proof theoretical consequences, the most important being the inability to design deductive systems. Since the object level is untouchable (it's the language you want to deal with), one can fix the problem by `improving ́ the meta level; or one can also sort of merge object and meta level by using deep inference. ...

Note (first note only)

• Concert Reading Group: 05/30/2005

Abstract

The atomic block, a synchronization primitive provided to programmers in transactional memory systems, has the potential to greatly ease the development of concurrent software. However, atomic blocks can still be used incorrectly, and race conditions can still occur at the level of application logic. In this paper, we present a intraprocedural static analysis, formalized as a type system and proven sound, that helps programmers use atomic blocks correctly. Using access permissions , which describe how objects are aliased and modified, ...

Note (first note only)

• Concert Reading Group: 09/29/2009

Note (first note only)

• Classic Papers: 09/21/2009 (William Lovas)

Note (first note only)

• Classic Papers: 09/14/2009 (Rob Simmons)

Note (first note only)

• Concert Reading Group: 09/15/2009 (Section 4.1-4.3 only were suggested reading to compliment Murphy`s Thesis which was the primary reading)

Note (first note only)

• Concert Reading Group: 09/15/2009 (Section 3.1-3.3 was the primary reading, Sections 1 and 2 were optional)

Abstract

We present ML5, a high level programming language for spatially distributed computing. The language, a variant of ML, allows an entire distributed application to be developed and reasoned about as a unified program. The language supports transparent mobility of any kind of code or data, but its type system, based on modal logic, statically excludes programs that use mobile resources unsafely. The ML5 compiler produces code for all of the hosts that may be involved in the computation. These hosts may ...

Abstract

A proof is given of the correctness of the algorithm “Find.” First, an informal description is given of the purpose of the program and the method used. A systematic technique is described for constructing the program proof during the process of coding it, in such a way as to prevent the intrusion of logical errors. The proof of termination is treated as a separate exercise. Finally, some conclusions relating to general programming methodology are drawn. ...

Note (first note only)

• Classic Papers: 09/09/2009 (Karl Crary)

Abstract

So-called “guarded commands” are introduced as a building block for alternative and repetitive constructs that allow nondeterministic program components for which at least the activity evoked, but possibly even the final state, is not necessarily uniquely determined by the initial state. For the formal derivation of programs expressed in terms of these constructs, a calculus will be be shown. ...

Note (first note only)

• Classic Papers: 09/09/2009 (Karl Crary)

Abstract

In this paper an attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of mathematics. This involves the elucidation of sets of axioms and rules of inference which can be used in proofs of the properties of computer programs. Examples are given of such axioms and rules, and a formal proof of a simple theorem is displayed. Finally, ...

Note (first note only)

• Classic Papers: 09/09/2009 (Karl Crary)

Abstract

In functional programming, fold is a standard operator that encapsulates a simple pattern of recursion for processing lists. This article is a tutorial on two key aspects of the fold operator for lists. First of all, we emphasize the use of the universal property of fold both as a proof principle that avoids the need for inductive proofs, and as a definition principle that guides the transformation of recursive functions into definitions using ...

Abstract

This paper presents a semantic space profiler for parallel functional programs. Building on previous work in sequential profiling, our tools help programmers to relate runtime resource use back to program source code. Unlike many profiling tools, our profiler is based on a cost semantics. This provides a means to reason about performance without requiring a detailed understanding of the compiler or runtime system. It also provides a specification for language implementers. This is critical in that it enables us to separate ...

Note (first note only)

• Concert Reading Group: 09/01/2009

Note (first note only)

• Concert Reading Group: 08/25/2009 (Chapters 1-4)

Abstract

The basis for this paper is a logic designed by Dana Scott [1] in 1969 for formalizing arguments about computable functions of higher type. This logic uses typed combinators, and we give a more or less direct translation into typed &lgr;-calculus, which is an easier formalism to use, though not so easy for the metatheory because of the presence of bound variables. We then describe, by example only, a proof-checker program which has been implemented for this logic; the program is ...

Note (first note only)

• Concert Reading Group: 08/18/2009, the 2009 Scavenger Hunt Reading Group

Abstract

Sentences in first-order predicate logic can be usefully interpreted as programs. In this paper the operational and fixpoint semantics of predicate logic programs are defined, and the connections with the proof theory and model theory of logic are investigated. It is concluded that operational semantics is a part of proof theory and that fixpoint semantics is a special case of model-theoretic semantics. ...

Note (first note only)

• Concert Reading Group: 08/18/2009, the 2009 Scavenger Hunt Reading Group

Abstract

This note is a discussion on David Spector's paper: "The Simplest Functional Programming Language" (SIGPLAN NOTICES18.1 (1983)). It is shown that neither syntax nor semantics of the referred language $ is simpler than that of the pure λ-calculus, and furthermore, this language does not meet the requirement of substitutivity of equivalence, which is essential for functional languages. ...

Note (first note only)

• Concert Reading Group: 08/18/2009, the 2009 Scavenger Hunt Reading Group

Abstract

We introduce a language based upon lambda calculus with products, coproducts and strictly positive inductive types that allows the definition of recursive terms. We present the implementation (foetus) of a syntactical check that ensures that all such terms are structurally recursive, i.e. recursive calls appear only with arguments structurally smaller than the input parameters of terms considered. To ensure the correctness of the termination checker, we show that all structurally recursive terms are normalizing with respect to a given operational semantics. ...

Note (first note only)

• Concert Reading Group: 08/11/2009

Note (first note only)

• Concert Reading Group: 07/14/2009

Abstract

A family of unimplemented computing languages is described that is intended to span differences of application area by a unified framework. This framework dictates the rules about the uses of user-coined names, and the conventions about characterizing functional relationships. Within this framework the design of a specific language splits into two independent parts. One is the choice of written appearances of programs (or more generally, their physical representation). The other is the choice of the abstract entities (such as numbers, character-strings, ...

Note (first note only)

• Concert Reading Group: 06/23/2009
• Classic Papers: 09/16/2009 (Ruy Ley-Wild)

Note (first note only)

• Concert Reading Group: 04/11/2005
• Concert Reading Group: 06/02/2009
• Classic Papers: 11/09/2009 (Rob Arnold)

Abstract

An abstract is not available. ...

Note (first note only)

• Concert Reading Group: 05/27/2009

Abstract

The discussion in the computer-science literature of the relative merits of linear- versus branching-time frameworks goes back to early 1980s. One of the beliefs dominating this discussion has been that the linear-time framework is not expressive enough semantically, making linear-time logics lacking in expressiveness. In this work we examine the branching-linear issue from the perspective of process equivalence, which is one of the most fundamental notions in concurrency theory, as defining a notion of process equivalence essentially amounts to defining semantics ...

Note (first note only)

• Concert Reading Group: 05/05/2009

Abstract

A Gentzen sequent calculus for Lax Logic is presented, the proofs in which correspond naturally in a 1–1 way to the normal natural deductions for the logic. The propositional fragment of this calculus is used as the basis for another calculus that uses a history mechanism in order to give a decision procedure for propositional Lax Logic. ...

Note (first note only)

• Concert Reading Group: 03/17/2009

Note (first note only)

• Concert Reading Group: 02/23/2009

Abstract

The method of logical relations assigns a relational interpretation to types that expresses operational invariants satisfied by all terms of a type. The method is widely used in the study of typed languages, for example to establish contextual equivalences of terms. The chief difficulty in using logical relations is to establish the existence of a suitable relational interpretation. We extend work of Pitts and Birkedal and Harper on constructing relational interpretations of types to polymorphism and recursive types, and apply it ...

Note (first note only)

• Concert Reading Group: 02/16/2009

Abstract

We have built the first family of tagless interpretations for a higher-order typed object language in a typed metalanguage (Haskell or ML) that require no dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value CPS transformers. Our main idea is to encode HOAS de Bruijn or higher-order abstract syntax using cogen functions rather than data constructors. In other words, we ...

Note (first note only)

• Concert Reading Group: 03/24/2008

Abstract

Tait's method (a.k.a. proof by logical relations) is a powerful proof technique frequently used for showing foundational properties of languages based on typed lambda-calculi.??Historically, these proofs have been extremely difficult to formalize in proof assistants with weak meta-logics, such as Twelf, and yet they are often straightforward in proof assistants with stronger meta-logics. In this paper, we propose structural logical relations as a technique for conducting these proofs in systems with limited meta-logical strength by explicitly representing and reasoning about an ...

Note (first note only)

• Concert Reading Group: 05/12/2008

Abstract

Certain principles are fundamental to operational semantics, regardless of the languages or idioms involved. Such principles include rule-based definitions and proof techniques for congruenceresults. We formulate these principles in the general context of categorical logic. From this general formulation we recover precise results for particular language idioms by interpreting the logic inparticular categories. For instance, results for first-order calculi, such as CCS, arise from considering the general results in the category of sets. Results for languages involving substitution and name generation, ...

Note (first note only)

• Concert Reading Group: 06/18/2008

Abstract

We introduce a systematic procedure to transform large classesof (Hilbert) axioms into equivalent inference rules in sequent and hypersequent calculi. This allows for the automated generation of analytic calculi for a wide range of propositional nonclassical logics including intermediate, fuzzy and substructural logics. Our work encompasses many existing results, allows for the definition of new calculi and contains a uniform semantic proof of cut-elimination for hypersequent calculi. ...

Note (first note only)

• Concert Reading Group: 08/18/2008

Abstract

The driving idea of functional programming is to make programming more closely related to mathematics. A program in a functional language such as Haskell or Miranda consists of equations which are both computation rules and a basis for simple algebraic reasoning about the functions and data structures they define. The existing model of functional programming, although elegant and powerful, is compromised to a greater extent than is commonly recognised by the presence of partial functions. We consider a simple discipline of ...

Note (first note only)

• Concert Reading Group: 08/24/2008

Abstract

There has been much work in recent years on extending ML with recursive modules. One of the most difficult problems in the development of such an extension is the double vision problem, which concerns the interaction of recursion and data abstraction. In previous work, I defined a type system called RTG, which solves the double vision problem at the level of a System-F-style core calculus. In this paper, I scale the ideas and techniques of RTG to the level ...

Note (first note only)

• Concert Reading Group: 12/10/2007