Theory

Decidability of Higher Order Matching

Decidability of Higher Order Matching, Colin Stirling.

Higher-order unification is the problem: given an equation t = u containing free variables, is there a solution substitution Θ such that tΘ and uΘ have the same normal form? The terms are drawn from the simply typed lambda calculus and the same normal form is up to βη-equality. Higher order matching is the particular instance: when the term u is closed, can t be pattern matched to u? Although higher-order unification is undecidable (even if free variables are only second-order), higher-order matching was conjectured to be decidable by Huet. [...] In this paper, we confirm Huet's conjecture that higher-order matching is decidable.

This paper is very technical, but I think it's a problem of significant interest, since decidable fragments of higher-order unification are very important to theorem proving systems. As an aside, Huet conjectured that higher order matching was decidable in 1976, so it's taken thirty years of effort to prove this.

Modular Verification of Assembly Code with Stack-Based Control Abstractions

Modular Verification of Assembly Code with Stack-Based Control Abstractions

by Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, Zhaozhong Ni

Published in Proc. 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'06), Ottawa, Canada, pages 401-414, June 2006. ©2006 ACM.

Abstract

Runtime stacks are critical components of any modern software---they are used to implement powerful control structures such as function call/return, stack cutting and unwinding, coroutines, and thread context switch. Stack operations, however, are very hard to reason about: there are no known formal specifications for certifying C-style setjmp/longjmp, stack cutting and unwinding, or weak continuations (in C--). In many proof-carrying code (PCC) systems, return code pointers and exception handlers are treated as general first-class functions (as in continuation-passing style) even though both should have more limited scopes.

In this paper we show that stack-based control abstractions follow a much simpler pattern than general first-class code pointers. We present a simple but flexible Hoare-style framework for modular verification of assembly code with all kinds of stack-based control abstractions, including function call/return, tail call, setjmp/longjmp, weak continuation, stack cutting, stack unwinding, multi-return function call, coroutines, and thread context switch. Instead of presenting a specific logic for each control structure, we develop all reasoning systems as instances of a generic framework. This allows program modules and their proofs developed in different PCC systems to be linked together. Our system is fully mechanized. We give the complete soundness proof and a full verification of several examples in the Coq proof assistant.

Of interest to those interested in verification, and the formal theory of stacks. Anyone else interested in seeing a new category created for assembly and intermediate languages?

Church’s Thesis and Functional Programming

David Turner gives a condensed summary of the lambda calculus and functional programming in this paper on Church’s Thesis and Functional Programming.

The lambda-calculus, which Church developed during the period of convergence from which the Thesis emerged, has influenced almost every aspect of the development of programming and programming languages. It is the basis of functional programming, which after a long infancy is entering adulthood as a practical alternative to traditional ad-hoc imperative programming languages. Many important ideas in mainstream programming languages—recursion, procedures as parameters, linked lists and trees, garbage collectors — came by cross fertilization from functional programming. Moreover the main schools of both operational and denotational semantics are lambda-calculus based and amount to using functional programming to explain other programming systems.

The original project from whose wreckage by paradox lambda-calculus survived, to unify logic with an account of computable functions, appears to have been reborn in unexpected form, via the propositions-as-types paradigm.

Many of the PLT topics mentioned on LtU are covered - PLT in 20 pages or less. I'm still hoping for someone to publish a pop-PLT book that takes something like these 20 pages and turns them into a 800 page novel. In the meantime, this is a nice roadmap for PLT that helps provide the connections between such things as Curry-Howard, Coq, System F. (About as close to a cheatsheet for LtU that I've come across).

A Logic for Parametric Polymorphism

A Logic for Parametric Polymorphism, Gordon Plotkin and Martín Abadi.

In this paper we introduce a logic for parametric polymorphism. Just as LCF is a logic for the simply-typed lambda-calculus with recursion and arithmetic, our logic is a logic for System F. The logic permits the formal presentation and use of relational parametricity. Parametricity yields --- for example --- encodings of initial algebras, final co-algebras and abstract datatypes, with corresponding proof principles of induction, co-induction and simulation.

Separation Logic courses (Reynolds)

For some reason (probably starting with the letter N), seperation logic was recently mentioned here a few times. Since this area may be relatively unknown to many readers, I thought the following two course web sites from John C. Reynolds may be of interest:

Separation Logic (Spring 2004)

Current Research on Separation Logic (Spring 2005)

RZ for Constructive Mathematics in Programming

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.

Annotated POPL 2007 Program

POPL 2007 is just around the corner, and the Little Calculist has taken time off from inventing Web 4.0 to track down all the papers available online, and collect them in an annotated program, Favourite titles: Proving That Programs Eventually Do Something Good, and Lazy Multivariate Higher-Order Forward-Mode AD. I have no idea what the later means, but I love the pile-up of jargon.

Seminar: Classical vs. Quantum Computation

Classical versus Quantum Computation. John Baez.

This fall, John Baez has been conducting a seminar on classical and quantum computation. So far they appear to have covered mostly foundations of classical computation (lambda calculus, CCCs, the fixed point theorem). It's interesting to see lambda calculus introduced to an audience already comfortable with category theory.

Excellent lecture notes are available for each week with a bit of supporting material, and there have been blog posts for each class on The n-Category Cafe (the most recent one is here). The blog posts have some extra discussion, and comments, of course.

The seminar continues in the spring and I'm sure people may want to follow along...

Natural Deduction Reading for Beginners

The most active members of LtU for the most part already have a solid foundation in logic. For the rest of us interested in language design, but who are not already logicians here is a brief reading list on logic, focusing on natural deduction, the preferred method of expressing type systems.

More experienced members of LtU may perhaps consider contributing to the discussion with comments on the suggested reading or alternative suggestions.

[Edit: removed A History of Natural Deduction and Elementary Logic Textbooks by Jeff Pelletier and added several new links as suggested by Charles Stewart and falcon.]

Second Life Faces Threat to its Virtual Economy

Second Life Faces Threat to its Virtual Economy

Groups of Second Life content creators were gathering digitally Tuesday to protest the dissemination of a program they worry could badly damage the virtual world's nascent economy.

The controversy gathered steam Monday when Linden Lab, which publishes Second Life, posted a blog alerting residents of the virtual world to the existence of a program or bot called CopyBot, which allows someone to copy any object in Second Life. That includes goods such as clothing that people purchase for their in-world avatars, and even the virtual PCs that computer giant Dell announced Tuesday it is going to sell in the digital world.

Related to this thread, especially my "Not Merely Predictable" post, as well as the various Lightweight Static Capabilities and Robust Composition threads. I'm absolutely convinced that a future language design will evolve to accomodate the development of distributed systems in which these kinds of issues are impossible to impose. Is it time to add an "object capability security" and/or "cooperation without vulnerability" (a great phrase from Mark Miller) category to LtU?

XML feed