Semantics
Vellvm: Formalizing the LLVM Intermediate Representation for Verified Program Transformations by Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic, POPL 2012
This paper presents Vellvm (verified LLVM), a framework for reasoning about programs expressed in LLVM's intermediate representation and transformations that operate on it. Vellvm provides a mechanized formal semantics of LLVM's intermediate representation, its type system, and properties of its SSA form. The framework is built using the Coq interactive theorem prover. It includes multiple operational semantics and proves relations among them to facilitate different reasoning styles and proof techniques.
To validate Vellvm's design, we extract an interpreter from the Coq formal semantics that can execute programs from LLVM test suite and thus be compared against LLVM reference implementations. To demonstrate Vellvm's practicality, we formalize and verify a previously proposed transformation that hardens C programs against spatial memory safety violations. Vellvm's tools allow us to extract a new, verified implementation of the transformation pass that plugs into the real LLVM infrastructure; its performance is competitive with the nonverified, adhoc original.
This obviously represents huge progress in marrying the theoretical benefits of tools like Coq with the practical benefits of tools like LLVM. We can only hope that this spurs further development in practical certified software development.
The Experimental Effectiveness of Mathematical Proof
The aim of this paper is twofold. First, it is an attempt to give an answer to the famous essay of Eugene Wigner about the unreasonable effectiveness of mathematics in the natural sciences [25]. We will argue that mathematics are not only reasonably effective, but that they are also objectively effective in a sense that can be given a precise meaning. For thatâ€”and this is the second aim of this paperâ€”we shall reconsider some aspects of Popperâ€™s epistemology [23] in the light of recent advances of proof theory [8, 20], in order to clarify the interaction between pure mathematical reasoning (in the sense of a formal system) and the use of empirical hypotheses (in the sense of the natural sciences).
The technical contribution of this paper is the prooftheoretic analysis of the problem (already evoked in [23]) of the experimental modus tollens, that deals with the combination of a formal proof of the implication U â‡’ V with an experimental falsification of V to get an experimental falsification of U in the case where the formulÃ¦ U and V express empirical theories in a sense close to Popperâ€™s. We propose a practical solution to this problem based on Krivineâ€™s theory of classical realizability [20], and describe a simple procedure to extract from a formal proof of U â‡’ V (formalized in classical secondorder arithmetic) and a falsifying instance of V a computer program that performs a finite sequence of tests on the empirical theory U until it finds (in finite time) a falsifying instance of U.
I thought I had already posted this, but apparently not.
Consider this paper the main gauntlet thrown down to those who insist that mathematical logic, the CurryHoward Isomorphism, etc. might be fine for "algorithmic code" (as if there were any other kind) but is somehow inapplicable the moment a system interacts with the "real" or "outside" world (as if software weren't real).
Update: the author is Alexandre Miquel, and the citation is "Chapitre du livre Anachronismes logiques, Ã paraÃ®tre dans la collection Logique, Langage, Sciences, Philosophie, aux Publications de la Sorbonne. Ã‰d.: Myriam Quatrini et Samuel TronÃ§on, 2010."
Nick Benton and Neel Krishnaswami, ICFP'11, A Semantic Model for Graphical User Interfaces:
We give a denotational model for graphical user interface (GUI) programming using the Cartesian closed category of ultrametric spaces. [..] We capture the arbitrariness of user input [..] [by a nondeterminism] â€œpowerspaceâ€ monad.
Algebras for the powerspace monad yield a model of intuitionistic linear logic, which we exploit in the definition of a mixed linear/nonlinear domainspecific language for writing GUI programs. The nonlinear part of the language is used for writing reactive streamprocessing functions whilst the linear sublanguage naturally captures the generativity and usage constraints on the various linear objects in GUIs, such as the elements of a DOM or scene graph.
We have implemented this DSL as an extension to OCaml, and give examples demonstrating that programs in this style can be short and readable.
This is an application of their (more squiggly) LICS'11 submission, Ultrametric Semantics of Reactive Programs. In both these cases, I find appealing the fact the semantic model led to a type system and a language that was tricky to find.
Lightweight Monadic Programming in ML
Many useful programming constructions can be expressed as monads. Examples include probabilistic modeling, functional reactive programming, parsing, and information flow tracking, not to mention effectful functionality like state and I/O. In this paper, we present a typebased rewriting algorithm to make programming with arbitrary monads as easy as using ML's builtin support for state and I/O. Developers write programs using monadic values of type M t as if they were of type t, and our algorithm inserts the necessary binds, units, and monadtomonad morphisms so that the program type checks. Our algorithm, based on Jones' qualified types, produces principal types. But principal types are sometimes problematic: the program's semantics could depend on the choice of instantiation when more than one instantiation is valid. In such situations we are able to simplify the types to remove any ambiguity but without adversely affecting typability; thus we can accept strictly more programs. Moreover, we have proved that this simplification is efficient (linear in the number of constraints) and coherent: while our algorithm induces a particular rewriting, all related rewritings will have the same semantics. We have implemented our approach for a core functional language and applied it successfully to simple examples from the domains listed above, which are used as illustrations throughout the paper.
This is an intriguing paper, with an implementation in about 2,000 lines of OCaml. I'm especially interested in its application to probabilistic computing, yielding a result related to Kiselyov and Shan's Hansei effort, but without requiring delimited continuations (not that there's anything wrong with delimited continuations). On a theoretical level, it's nice to see such a compelling example of what can be done once types are freed from the shackle of "describing how bits are laid out in memory" (another such compelling example, IMHO, is typedirected partial evaluation, but that's literally another story).
Andrej Bauer's blog contains the PL Zoo project. In particular, the Levy language, a toy implementation of Paul Levy's CBPV in OCaml.
If you're curious about CBPV, this implementation might be a nice accompaniment to the book, or simply a hands on way to check it out.
It looks like an implementation of CBPV without sum and product types, with complex values, and without effects. I guess a more handson way to get to grips with CBPV would be to implement any of these missing features.
The posts are are 3 years old, but I've only just noticed them. The PL Zoo project was briefly mentioned here.
Imperative Programs as Proofs via Game Semantics, Martin Churchill, James Laird and Guy McCusker. To appear at LICS 2011.
Game semantics extends the CurryHoward isomorphism to a threeway correspondence: proofs, programs, strategies. But the universe of strategies goes beyond intuitionistic logics and lambda calculus, to capture stateful programs. In this paper we describe a logical counterpart to this extension, in which proofs denote such strategies. We can embed intuitionistic ï¬rstorder linear logic into this system, as well as an imperative total programming language. The logic makes explicit use of the fact that in the game semantics the exponential can be expressed as a ï¬nal coalgebra. We establish a full completeness theorem for our logic, showing that every bounded strategy is the denotation of a proof.
This paper increases the importance of gaining a morethancasual understanding of game semantics for me, since it combines two of my favorite things: polarized type theories and imperative higherorder programs.
Macros that Work Together  CompileTime Bindings, Partial Expansion, and Definition Contexts, Matthew Flatt, Ryan Culpepper, David Darais, and Robert Bruce Findler. Under consideration for publication in J. Functional Programming.
Racket (formerly PLT Scheme) is a large language that is built mostly within itself. Unlike the usual
approach taken by nonLisp languages, the selfhosting of Racket is not a matter of bootstrapping
one implementation through a previous implementation, but instead a matter of building a tower of
languages and libraries via macros. The upper layers of the tower include a class system, a component
system, pedagogic variants of Scheme, a statically typed dialect of Scheme, and more. The demands
of this languageconstruction effort require a macro system that is substantially more expressive than
previous macro systems. In particular, while conventional Scheme macro systems handle standalone
syntactic forms adequately, they provide weak support for macros that share information or macros
that use existing syntactic forms in new contexts.
This paper describes and models novel features of the Racket macro system, including support for
general compiletime bindings, subform expansion and analysis, and environment management. The
presentation assumes a basic familiarity with Lispstyle macros, and it takes for granted the need for
macros that respect lexical scope. The model, however, strips away the pattern and template system
that is normally associated with Scheme macros, isolating a core that is simpler, that can support
pattern and template forms themselves as macros, and that generalizes naturally to Racketâ€™s other
extensions.
A good description of Racket's rocket science tools for growing languages.
Edward Fredkin and Tommoasso Toffoli from the MIT Labratory for Computer Science present Conservative Logic...
a comprehensive model of computation which explicitly reflects a number of fundamental principles of physics, such as the reversibility of the dynamical laws and the conservation of certain additive quantities (among which energy plays a distinguished role). Because it more closely mirrors physics than traditional models of computation, conservative logic is in a better position to provide indications concerning the realization of highperformance computing systems, i.e., of systems that make very efficient use of the "computing resources" actually offered by nature. In particular, conservative logic shows that it is ideally possible to build sequential circuits with zero internal power dissipation. After establishing a general framework, we discuss two specific models of computation. The first uses binary variables and is the conservativelogic counterpart of switching theory; this model proves that universal computing capabilities are compatible with the reversibility and conservation constraints. The second model, which is a refinement of the first, constitutes a substantial breakthrough in establishing a correspondence between computation and physics. In fact, this model is based on elastic collisions of identical "balls," and thus is formally identical with the atomic model that underlies the (classical) kinetic theory of perfect gases. Quite literally, the functional behavior of a generalpurpose digital computer can be reproduced by a perfect gas placed in a suitably shaped container and given appropriate initial conditions.
This paper has a small discussion in a forum thread mostly saying the paper should be on the front page.
Matthew Might, "Abstract interpreters for free", Static Analysis Symposium 2010 (SAS 2010).
...we present a twostep method to convert a smallstep concrete semantics into a family of sound, computable abstract interpretations. The first step refactors the concrete statespace to eliminate recursive structure; this refactoring of the statespace simultaneously determines a storepassingstyle transformation on the underlying concrete semantics. The second step uses inference rules to generate an abstract statespace and a Galois connection simultaneously. The Galois connection allows the calculation of the â€œoptimalâ€ abstract interpretation. The twostep process is unambiguous, but nondeterministic: at each step, analysis designers face choices. Some of these choices ultimately influence properties such as flow, field and contextsensitivity. Thus, under the method, we can give the emergence of these properties a graphtheoretic characterization.
The work in this paper provides some context for known static analysis techniques like kCFA, and also opens up some interesting new directions for static analysis development. Also, as Matt points out, there are some pedagogical benefits to having a systematic process for getting from semantics to abstract interpretation.
What Sequential Games, the Tychonoff Theorem, and the DoubleNegation Shift have in Common, Martin Escardo and Paulo Oliva, to appear in MSFP 2010.
This is a tutorial for mathematically inclined functional programmers, based on previously published, peered reviewed theoretical work. We discuss a highertype functional, written here in the functional programming language Haskell, which
 optimally plays sequential games,
 implements a computational version of the Tychonoff Theorem from topology, and
 realizes the DoubleNegation Shift from logic and proof theory.
The functional makes sense for finite and infinite (lazy) lists, and in the binary case it amounts to an operation that is available in any (strong) monad.
In fact, once we define this monad in Haskell, it turns out that this amazingly versatile functional is already available in Haskell, in the standard prelude, called sequence , which iterates this binary operation. Therefore Haskell proves that this functional is even more versatile than anticipated, as the function sequence was introduced for other purposes by the language designers, in particular the iteration of a list of monadic effects (but effects are not what we discuss here).
One of the most durable and productive analogies in semantics is the analogy between computability and continuity. Depending on how you read the history, this idea might even predate computers: Brouwer proved that all intuitonistic functions on the reals were continuous.
Over the last few years, Escardo and his collaborators have done a lot of cool stuff showing how this network of ideas can be turned into miraculouslooking little programs, so it's very nice to see a relatively accesible introduction to this work.

Recent comments
4 hours 23 min ago
2 weeks 2 days ago
2 weeks 2 days ago
3 weeks 3 days ago
3 weeks 3 days ago
3 weeks 3 days ago
3 weeks 3 days ago
3 weeks 3 days ago
4 weeks 2 days ago
4 weeks 3 days ago