Lambda the Ultimate

Gradual Typing for Objects. Jeremy Siek and Walid Taha.

Static and dynamic type systems have well-known strengths and weaknesses. In previous work we developed a gradual type system for a functional calculus named [...]. Gradual typing provides the benefits of both static and dynamic checking in a single language by allowing the programmer to control whether a portion of the program is type checked at compile-time or run-time by adding or removing type annotations on variables. Several object-oriented scripting languages are preparing to add static checking. To support that work this paper develops [another calculus], a gradual type system for object-based languages, extending the [...] calculus of Abadi and Cardelli. Our primary contribution is to show that gradual typing and subtyping are orthogonal and can be combined in a principled fashion. We also develop a small-step semantics, provide a machine-checked proof of type safety, and improve the space efficiency of higher-order casts.

The authors' previous work on gradual typing was discussed here. This brings it to an object-oriented setting which is (as the abstract points out) very directly applicable to mainstream scripting languages, at least in principle.

[Edit: This is from the types list, where the authors also added: "We will present the paper at ECOOP 2007 and would be especially interested in any feedback on the paper before the final submission is due on April 25."]

RZ for Constructive Mathematics in Programming by Chris Stone and Andrej Bauer.

Realizability theory is not only a fundamental tool in logic and computability, but also has direct application to the design and implementation of programs: it can produce interfaces for the data structure corresponding to a mathematical theory. Our tool, called RZ, serves as a bridge between the worlds of constructive mathematics and programming. By using the realizability interpretation of constructive mathematics, RZ translates specifications in constructive logic into annotated interface code in Objective Caml. The system supports a rich input language allowing descriptions of complex mathematical structures. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools.

I haven't read the paper yet, but the abstract reminded me of PADS.

Separation Logic: A Logic for Shared Mutable Data Structure, John C. Reynolds. LICS 2002

In joint work with Peter O'Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure.

The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a "separating conjunction" that asserts that its subformulas hold for disjoint parts of the heap, and a closely related "separating implication". Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing.

I think this paper has been mentioned several times in discussion on LtU, but never gotten an article of its own. It's a really elegant piece of work that addresses the biggest weakness of Hoare logic: that you cannot do local, modular correctness proofs of programs that use aliasable state.

(I should say my own research is on using separation logic in languages like ML or Haskell, so I am a partisan!)

Ott—a tool for writing definitions of programming languages and calculi.

Ott is a tool for writing definitions of programming languages and calculi. It takes as input a definition of a language syntax and semantics, in a concise and readable ASCII notation that is close to what one would write in informal mathematics. It generates LaTeX to build a typeset version of the definition, and Coq, HOL, and Isabelle versions of the definition. Additionally, it can be run as a filter, taking a LaTeX/Coq/Isabelle/HOL source file with embedded (symbolic) terms of the defined language, parsing them and replacing them by target-system terms. For a simple example, here is an Ott source file for an untyped call-by-value lambda calculus (test10.ott), and the generated LaTeX (compiled to pdf) and (compiled to ps), Coq, Isabelle, and HOL definitions.

Most simply, the tool can be used to aid completely informal LaTeX mathematics. Here it permits the definition, and terms within proofs and exposition, to be written in a clear, editable, ASCII notation, without LaTeX noise. It generates good-quality typeset output. By parsing (and so sort-checking) this input, it quickly catches a range of simple errors, e.g. inconsistent use of judgement forms or metavariable naming conventions.

That same input can be used to generate formal definitions, for Coq, HOL, and Isabelle. It should thereby enable a smooth transition between use of informal and formal mathematics. Additionally, the tool can automatically generate definitions of functions for free variables, single and multiple substitutions, subgrammar checks (e.g. for value subgrammars), and binding auxiliary functions. (At present only a fully concrete representation of binding is supported, without quotienting by alpha equivalence.)

The distribution includes several examples, in varying levels of completeness: untyped and simply typed lambda-calculus, a calculus with ML polymorphism, the POPLmark Fsub with and without records, an ML module system taken from (Leroy, JFP 1996) and equipped with an operational semantics, and LJ, a lightweight Java fragment.

Peter Sewell and his team continue to bridge the gap between the informal and formal worlds of programming language semantics.

Locus Solum: From the rules of logic to the logic of rules by Jean-Yves Girard, 2000.

The monograph below has been conceived as the project of giving reasonable foundations to logic, on the largest possible grounds, but not with the notorious reductionist connotation usually attached to "foundations". Locus Solum would like to be the common playground of logic, independent of systems, syntaxes, not to speak of ideologies. But wideness of scope is nothing here but the reward of sharpness of concern : I investigate the multiple aspects of a single artifact, the design. Designs are not that kind of syntax-versus-semantics whores that one can reshape according to the humour of the day : one cannot tamper with them, period. But what one can achieve with them, once their main properties —separation, associativity, stability— have been understood, is out of proportion with their seemingly banal definition.

Sounds rather controversial, but can make an interesting reading if you believe logic is related to programming (your last name doesn't have to be either Curry or Howard).

Beauty in the Beast by Wouter Swierstra, Thorsten Altenkirch. 2006.

We provide a functional specification of three central components of Simon Peyton Jones’s awkward squad: teletype I/O, mutable state and concurrency. By constructing an internal model of such concepts within our programming language, we can reason about programs that perform I/O as if they were pure functions. One important application of our approach is accommodating I/O in a dependently typed programming language.

A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations by Dariusz Biernacki, Olivier Danvy, Kevin Millikin. 2006.

Compared to static delimited continuations, and despite recent implementation advances, the topic of dynamic delimited continuations still remains largely unexplored. We believe that the spectrum of compatible computational artifacts presented here — abstract machine, evaluator, computational monad, and dynamic continuation-passing style — puts one in a better position to assess them.

An Axiomatic Basis for Computer Programming by Tony Hoare, 1969.

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, it is argued that important advantage, both theoretical and practical, may follow from a pursuance of these topics.

Considered by many to be among the best of the great works in programming languages.

by James Cheney (beware, PDF takes up full screen)

Based on envious observations of the success of formal methods for verifying industrial hardware designs using model-checking, I will argue that "partial" techniques which provide full automation and search for counterexamples, but which do not try to verify correctness, are likely to be more useful [for "metatheory of logics and programming languages"] on a day-to-day basis activities than full verification. I will describe an unsophisticated, yet useful, implementation of such a "model-checking" approach to mechanized metatheory implemented using nominal logic programming (although the basic idea could be employed in many other settings).

Model checking meets POPLMark. I can't tell from this presentation if there's any chance of using tools similar to BLAST to search deeper or produce actual proofs.

A draft by Takeuti Izumi

This paper defines the theories of parametricity for the system lambda-P-omega in lambda cube, and shows some of its application. These theories are defined by the axiom sets in the formal theories. These theories prove various important semantical properties in the formal systems.

Parametricity is Wadler gets his theorems for free, nad Izumi gives an example of one of these free theorems for dependent sums in the Calculus of Constructions.