Semantics
In case this one went under the radar, at POPL'12, Martín Escardó gave a tutorial on seemingly impossible functional programs:
Programming language semantics is typically applied to
prove compiler correctness and allow (manual or automatic) program
verification. Certain kinds of semantics can also be applied to
discover programs that one wouldn't have otherwise thought of. This is
the case, in particular, for semantics that incorporate topological
ingredients (limits, continuity, openness, compactness). For example,
it turns out that some function types (X > Y) with X infinite (but
compact) do have decidable equality, contradicting perhaps popular
belief, but certainly not (highertype) computability theory. More
generally, one can often check infinitely many cases in finite time.
I will show you such programs, run them fast in surprising instances,
and introduce the theory behind their derivation and working. In
particular, I will study a single (very high type) program that (i)
optimally plays sequential games of unbounded length, (ii) implements
the Tychonoff Theorem from topology (and builds finitetime search
functions for infinite sets), (iii) realizes the doublenegation shift
from proof theory (and allows us to extract programs from classical
proofs that use the axiom of countable choice). There will be several
examples in the languages Haskell and Agda.
A shorter version (coded in Haskell) appears in Andrej Bauer's blog.
In his blog, Bob Harper, in joint effort with Dave MacQueen and Lars Bergstrom, announces the launch of smlfamily.org:
The Standard ML Family project provides a home for online versions of various formal definitions of Standard ML, including the "Definition of Standard ML, Revised" (Standard ML 97). The site also supports coordination between different implementations of the Standard ML (SML) programming language by maintaining common resources such as the documentation for the Standard ML Basis Library and standard test suites. The goal is to increase compatibility and resource sharing between Standard ML implementations.
The site includes a history section devoted to the history of ML, and of Standard ML in particular. This section will contain a collection of original source documents relating to the design of the language.
Logical methods in computer science just published Matija Pretnar's latest take on algebraic effects and handlers:
We present a complete polymorphic effect inference algorithm for an MLstyle language with handlers of not only exceptions, but of any other algebraic effect such as input & output, mutable references and many others. Our main aim is to offer the programmer a useful insight into the effectful behaviour of programs. Handlers help here by cutting down possible effects and the resulting lengthy output that often plagues precise effect systems. Additionally, we present a set of methods that further simplify the displayed types, some even by deliberately hiding inferred information from the programmer.
Pretnar and Bauer's Eff has made previous appearances here on LtU. Apart from the new fangled polymorphic effect system, this paper also contains an Eff tutorial.
Earlier this week Microsoft Research Cambridge organised a Festschrift for Luca Cardelli. The preface from the book:
Luca Cardelli has made exceptional contributions to the world of programming
languages and beyond. Throughout his career, he has reinvented himself every
decade or so, while continuing to make true innovations. His achievements span
many areas: software; language design, including experimental languages;
programming language foundations; and the interaction of programming languages
and biology. These achievements form the basis of his lasting scientific leadership
and his wide impact.
...
Luca is always asking "what is new", and is always looking to
the future. Therefore, we have asked authors to produce short pieces that would
indicate where they are today and where they are going. Some of the resulting
pieces are short scientific papers, or abridged versions of longer papers; others are
less technical, with thoughts on the past and ideas for the future. We hope that
they will all interest Luca.
Hopefully the videos will be posted soon.
Conor McBride gave an 8lecture summer course on Dependently typed metaprogramming (in Agda) at the Cambridge University Computer Laboratory:
Dependently typed functional programming languages such as Agda are capable of expressing very precise types for data. When those data themselves encode types, we gain a powerful mechanism for abstracting generic operations over carefully circumscribed universes. This course will begin with a rapid depedentlytyped programming primer in Agda, then explore techniques for and consequences of universe constructions. Of central importance are the â€œpattern functorsâ€ which determine the node structure of inductive and coinductive datatypes. We shall consider syntactic presentations of these functors (allowing operations as useful as symbolic differentiation), and relate them to the more uniform abstract notion of â€œcontainerâ€. We shall expose the doublelife containers lead as â€œinteraction structuresâ€ describing systems of effects. Later, we step up to functors over universes, acquiring the power of inductiverecursive definitions, and we use that power to build universes of dependent types.
The lecture notes, code, and video captures are available online.
As with his previous course, the notes contain many(!) mind expanding exploratory exercises, some of which quite challenging.
The Milner Symposium 2012 was held in Edinburgh this April in memory of the late Robin Milner.
The Milner Symposium is a celebration of the life and work of one of the world's greatest computer scientists, Robin Milner. The symposium will feature leading researchers whose work is inspired by Robin Milner.
The programme consisted of academic talks by colleagues and past students. The talks and slides are available online.
I particularly liked the interleaving of the personal and human narrative underlying the scientific journey. A particularly good example is Joachim Parrow's talk on the origins of the pi calculus. Of particular interest to LtU members is the panel on the future of functional programming languages, consisting of Phil Wadler, Xavier Leroy, David MacQueen, Martin Odersky, Simon PeytonJones, and Don Syme.
Mechanized Î»_{JS}
The Brown PLT Blog, 20120604
In an earlier post, we introduced Î»_{JS}, our operational semantics for JavaScript. Unlike many other operational semantics, Î»_{JS} is no toy, but strives to correctly model JavaScript's messy details. To validate these claims, we test Î»_{JS} with randomly generated tests and with portions of the Mozilla JavaScript test suite.
Testing is not enough. Despite our work, other researchers found a missing case in Î»_{JS}. Today, we're introducing Mechanized Î»_{JS}, which comes with a machinechecked proof of correctness, using the Coq proof assistant.
More work on mechanizing the actual, implemented semantics of a real language, rather than a toy.
Tool Demo: ScalaVirtualized
This paper describes ScalaVirtualized, which extends the Scala language and compiler with a small number of features that enable combining the beneï¬ts of shallow and deep embeddings of DSLs. We demonstrate our approach by showing how to embed three different domainspeciï¬c languages in Scala. Moreover, we summarize how others have been using our extended compiler in their own research and teaching. Supporting artifacts of our tool include webbased tutorials, nightly builds, and an Eclipse update site hosting an uptodate version of the Scala IDE for Eclipse based on the Virtualized Scala compiler and standard library.
Scala has always had a quite good EDSL story thanks to implicits, dot and pareninference, and methodsasoperators. Lately there are proposals to provide it with both macrosinthecamlp4sense and support for multistage programming. This paper goes into some depth on the foundations of the latter subject.
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."

Recent comments
3 hours 40 min ago
7 hours 49 min ago
9 hours 55 min ago
13 hours 36 min ago
23 hours 50 min ago
1 day 36 min ago
1 day 3 hours ago
1 day 9 hours ago
1 day 13 hours ago
1 day 15 hours ago