Theory
Sliced bananas on opaque data (The expression lemma). Ralf Lämmel and Ondrej Rypacek.
Algebraic data types and catamorphisms (folds) play a central role in functional programming as they allow programmers to define recursive data structures and operations on them uniformly by structural recursion. Likewise, in object-oriented (OO) programming, recursive hierarchies of object types with virtual methods play a central role for the same reason. There is a semantical correspondence between these two situations which we reveal and formalize categorically. To this end, we assume a coalgebraic model of OO programming with functional objects. In practical terms, the development prepares for refactorings that turn sufficiently disciplined functional folds into OO programs of a designated shape (and v.v.).
I haven't even glanced at the paper yet, but it looks extremely interesting, and it's directly related to some recent discussion. This blog post from Ondrej is also relevant.
Relating Complexity and Precision in Control Flow Analysis, David Van Horn and Harry Mairson. ICFP 2007.
We analyze the computational complexity of kCFA, a hierarchy of control flow analyses that determine which functions may be applied at a given call-site. This hierarchy specifies related decision problems, quite apart from any algorithms that may implement their solutions. We identify a simple decision problem answered by this analysis and prove that in the 0CFA case, the problem is complete for polynomial time. The proof is based on a nonstandard, symmetric implementation of Boolean logic within multiplicative linear logic (MLL). We also identify a simpler version of 0CFA related to eta-expansion, and prove that it is complete for logarithmic space, using arguments based on computing paths and permutations.
For any fixed k > 0, it is known that kCFA (and the analogous decision problem) can be computed in time exponential in the program size. For k = 1, we show that the decision problem is NP-hard, and sketch why this remains true for larger fixed values of k. The proof technique depends on using the approximation of CFA as an essentially nondeterministic computing mechanism, as distinct from the exactness of normalization. When k = n, so that the "depth" of the control flow analysis grows linearly in the program length, we show that the decision problem is complete for exponential time.
In addition, we sketch how the analysis presented here may be extended naturally to languages with control operators. All of the insights presented give clear examples of how straightforward observations about linearity, and linear logic, may in turn be used to give a greater understanding of functional programming and program analysis.
There's ton of really good stuff in here; I was particularly fascinated by the fact that 0-CFA is exact for multiplicatively linear programs (ie, that use variables at most once), because linearity guarantees that every lambda can flow to at most one use site.
A Model for Formal Parametric Polymorphism: A PER Interpretation for System R , Roberto Bellucci, Martin Abadi, Pierre-Louis Curien. TLCA 1995
System R is an extension of system F that formalizes Reynolds' notion of relational parametricity. In system R, considerably more lambda-terms can be proved equal than in system F: for example, the encoded weak products of F are strong products in R. Also, many "theorems for free" à la Wadler can be proved formally in R. In this paper we describe a semantics for system R. As a first step, we give a precise 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.
System R is a logic for proving relational parametricity results. It's similar in some ways to Abadi-Plotkin logic, which we have linked to previously on LtU.
Aydemir, Charguéraud, Pierce, Pollack, and Weirich. Engineering Formal Metatheory.
Machine-checked proofs of properties of programming languages have become a critical need, both for increased confidence in large and complex designs and 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. The representation and manipulation of terms with variable binding is a key issue.
We propose a novel style for formalizing metatheory, combining locally nameless representation of terms and cofinite quantification of free variable names in inductive definitions of relations on terms (typing, reduction, . . . ). ... We have carried out several large developments in this style using the Coq proof assistant and have made them publicly available. Our developments include type soundness for System F<: and core ML (with references, exceptions, datatypes, recursion, and patterns) and subject reduction for the Calculus of Constructions.
A fairly recent paper from the POPLmark team, which describes an approach to formalizing programming metatheory that they think performs well on the POPLmark challenge criteria (low formalization overhead, low cost of entry, and reasonable similarity to existing informal proof techniques). It looks like this is related to some of the material presented in the How to write your next POPL paper in Coq tutorial at POPL'08, which was previously mentioned on LtU.
A Dialogue on Infinity, between a mathematician and a philosopher. Alexandre Borovik and David Corfield.
A new blog... From the first post:
The project concentrates on one of the principal purposes of the Exploring the Infinite Program:
To understand the nature of and the role played by conceptualizations of infinity in mathematics.
It will be shaped as a dialogue between a mathematician (AB) and a philosopher (DC) and will address one of the central paradoxes of mathematics:
why are most uses of infinity in mathematics restricted to the recycling of a small number of “canonical” and ubiquitous structures?
...To put the study of infinity on a firm basis, we first have to discuss the issue of the identity and “sameness” of mathematical objects: infinity of what?
This is pretty far out for LtU, but I suspect it will interest some more philosophically inclined readers. They will look at a number of disciplines, including computer science.
(I feel like maybe even "Theory" is not theoretical for this. Therefore I am also calling it "Fun".)
If this sounds like a worthy goal, or if you are simply interested in the use of proof assistants for rogramming language research, you don't want to miss upcoming tutorial.
OCaml Light: a formal semantics for a substantial subset of the Objective Caml language.
OCaml light is a formal semantics for a substantial subset of the Objective Caml language. It is written in Ott, and it comprises a small-step operational semantics and a syntactic, non-algorithmic type system. A type soundness theorem has been proved and mechanized using the HOL-4 proof assistant, thereby ensuring that the proof is free from errors. To ensure that the operational semantics accurately models Objective Caml, an executable version of the semantics has been created (and proved equivalent in HOL to the original, relational version) and tested on a number of small test cases.
Note that while we have tried to make the semantics accurate, we are not part of the OCaml development team - this is in no sense a normative specification of the implemented language.
From a team including Peter Sewell (Acute, HashCaml, Ott).
I continue to believe that things are heating up nicely in mechanized metatheory, which, in the multicore/multiprocessor world in which we now live, is extremely good news.
Davide Sangiorgi, On the origins of Bisimulation, Coinduction, and Fixed Points.
The origins of bisimulation and bisimilarity are examined, in the three fields where they have been independently discovered: Computer Science, Philosophical Logic (precisely, Modal Logic), Set Theory.
Bisimulation and bisimilarity are coinductive notions, and as such are intimately related to fixed points, in particular greatest fixed points. Therefore also the appearance of coinduction and fixed points are discussed, though in this case only within Computer Science. The paper ends with some historical remarks on the main fixed-point theorems (such as Knaster-Tarski) that underpin the fixed-point theory presented.
There is a wealth of interesting information in this paper. Alas, it is not very easy to read, and the exposition can be improved. So this is not for beginners or outsiders, but if you are familiar with the topic the historical discussion will be of interest.
Lifting Abstract Interpreters to Quantified Logical Domains. Sumit Gulwani, Bill McCloskey, Ashish Tiwari. July 2007.
Today, abstract interpretation is capable of inferring a wide variety of quantifier-free program invariants. In this paper, we describe a general technique for building powerful quantified abstract domains that leverage existing quantifier-free domains. For example, from a domain that abstracts facts like "a[1] = 0", we automatically construct a domain that can represent universally quantified facts like "Forall i: (0 <= i < n) => A[i]=0)". The principal challenge in building such a domain is that, while most domains supply over-approximations of operations like join, meet, and variable elimination, working with the guards of quantified facts requires under-approximation...
Using our generic construction, we build a number of abstract interpreters on top of domains for linear arithmetic, uninterpreted function symbols (used to model heap accesses), and pointer reachability. Our experiments on a variety of programs using arrays and pointers (including several sorting algorithms) demonstrate the feasibility of the approach on challenging examples.
Validity Invariants and Effects, Yi Lu, John Potter and Jingling Xue. ECOOP 2007.
Object invariants describe the consistency of object states, and are crucial for reasoning about the correctness of object-oriented programs. However, reasoning about object invariants in the presence of object abstraction and encapsulation, arbitrary object aliasing and re-entrant method calls, is difficult. We present a general framework for reasoning about object invariants based on a behavioural abstraction that specifies two sets---the validity invariant, representing objects that must be valid before and after the behaviour, and the validity effect, describing objects that may be invalidated during the behaviour. The overlap of these two sets is critical because it captures precisely those objects that need to be re-validated at the end of the behaviour. When there is no overlap, no further validity checking is required. We also present a type system based on this framework. This system uses ownership types to confine dependencies for object invariants, and restricts permissible updates to track where object invariants hold even in the presence of re-entrant calls, but otherwise object referenceability and read access are not restricted.
I really liked this paper, but I think it might need a few preliminary explanations. There's a style of verification of OO programs based on "object invariants", which is the idea that you ensure that each object has an invariant, which every method maintains. Then verification is local, in the sense that you can verify each class's invariants independently. (This is used in the Boogie methodology used by Spec#, for instance.)
However, there are a couple of wrinkles. First, aliasing: every object's invariant depends on some of the objects in its fields, and you don't want random aliases letting strangers modify your representation objects underneath your feet. So you introduce a notion of ownership to help track who has permission to mess with each object. Second, reentrancy: suppose the middle of a method body has temporarily broken the object's invariant, and you call another method on the object? You don't a priori know the call is safe.
The type system the authors have introduced here tracks ownership and possibly-dangerous reentrant calls. The really clever part is that instead of just rejecting programs that fail these checks, they log all of the places where things break. So instead of saying "yes" or "no", the type system says "yes" or "manually verify the following things". So it's a labor-saving device for a verification methodology.
 |
