rain * oatdoors .
We enjoyed careful study of hieroglyphic writing systems and other complex calculational notations, which we look forward to continuing at the next meeting - provided that the world doesn't end on 23rd December 2012.
Les membres du WG2.1 et les observateurs pr\xE9sents \xE0 la 69e r\xE9union \xE0 Ottawa tiennent \xE0 exprimer leur Action de gr\xE2ces envers Rick Hehner de l'Universit\xE9 de Toronto et \xE0 Margaret Jackson pour avoir organis\xE9 une r\xE9union extraordinaire dans cette belle capitale. Ils ont m\xEAme soigneusement sp\xE9cifi\xE9 le temps de l'excursion
pluie * grain' air .
Nous avons appr\xE9ci\xE9 une \xE9tude approfondie des syst\xE8mes d'\xE9criture hi\xE9roglyphiques et d'autres notations complexes de calcul, que nous nous r\xE9jouissons de continuer \xE0 la prochaine r\xE9union - \xE0 condition que le monde ne s'arr\xEAte pas le 23 D\xE9cembre 2012.
This paper presents a more structured approach to the reuse of formalizations of programming language semantics through the composition of modular definitions and proofs. The key contribution is the development of an approach to induction for extensible Church encodings which uses a novel reinterpretation of the universal property of folds. These encodings provide the foundation for a framework, formalized in Coq, which uses type classes to automate the composition of proofs from modular components.
Several interesting language features, including binders and general recursion, illustrate the capabilities of our framework. We reuse these features to build fully mechanized definitions and proofs for a number of languages, including a version of mini-ML. Bounded induction enables proofs of properties for non-inductive semantic functions, and mediating type classes enable proof adaptation for more feature-rich languages
A paper describing this work has recently been accepted at POPL 2013 http://users.ugent.be/~tschrijv/Research/papers/popl2013.pdf.$ Janis Voigtländer, Discoverung Counterexamples (and Proof Ingredients) for Knuth-like 0-1-...-k principles (Tuesday, October 9, 2012, 10:43): Knuth's 0-1-principle establishes that comparison-swap algorithms that sort correctly on the Booleans also sort correctly on arbitrary totally ordered value sets. A few years ago, I proved a similar statement for parallel prefix algorithms, but requiring 0-1-2 instead of only 0-1 ("Much Ado about Two", POPL'08). There is an interesting story (not told in that paper) about how I found that 0-1 is not enough, that 0-1-2 might be enough, and how I then found (the ingredients needed for) the key lemmas and then overall proof of the result. Namely, all that was found by rather brute force search, exploring combinatorics and properties of small-sized semigroups. I am now trying to write that story (with help from my student Moritz F\xFCrneisen), but this time using a more declarative approach for the discovery process by systematically transforming naive problem statements into ones that can be handled by QuickCheck and/or SmallCheck. $ Patrik Jansson, Functional Enumeration of Algebraic Types (Tuesday, October 9, 2012, 11:41): In mathematics, an enumeration of a set S is a bijective function from (an initial segment of) the natural numbers to S. We define "functional enumerations" as efficiently computable such bijections. This talk describes a theory of functional enumeration and provides an algebra of enumerations closed under sums, products, guarded recursion and bijections. We partition each enumerated set into numbered, finite subsets of elements of the same size. Feat provides efficient "random access" to values of any desired size. The primary application is property based testing, where it can be used to define any mix of random sampling (for example QuickCheck generators) and exhaustive enumeration (in the style of SmallCheck). For more details see http://wiki.portal.chalmers.se/cse/pmwiki.php/FP/Testing-Feat . (There is a paper about this in the Haskell Symposium 2012.) $ Ralf Hinze, The computational essence of sorting algorithms (Tuesday, October 9, 2012, 16:10): Sorting algorithms are an intrinsic part of functional programming folklore as they exemplify algorithm design using folds and unfolds. This has given rise to an informal notion of duality among sorting algorithms: insertion sorts are dual to selection sorts. Using bialgebras and distributive laws, we formalise this notion within a categorical setting. We use types as a guiding force in exposing the recursive structure of bubble, insertion, selection, quick, tree, and heap sorts. Moreover, we show how to distill the computational essence of these algorithms down to one-step operations that are expressed as natural transformations.
This is joint work with Daniel W.H. James, Thomas Harper, Nicolas Wu, Jos\xE9 Pedro Magalh\xE3es.$ Akimasa Morihata, Calculating parallel algorithms for size-constrained segment problems (Tuesday, October 9, 2012, 17:24): We study size-constrained segment problems: given an array, we calculate a value (e.g., maximum of the summations) from its consecutive subregions whose sizes are in a certain range. This kind of problems have several applications including knowledge mining and image processing, and the size constraint is useful for excluding useless solutions. While efficient sequential algorithms for them are known, efficient parallel algorithms have not been developed.
In this talk, we calculationally develop efficient parallel algorithms for size-constrained segment problems. We first consider enumerating summaries of segments of certain size, and develop a divide-and-conquer parallel algorithm for it. Then, we confirm that calculations based on the Bird-Meertens formalism bring efficient parallel algorithms for more involved problems.
The major part of the results was presented in FLOPS 2012. This talk slightly extends them.$ Yanhong A. Liu, From Clarity to Efficiency for Distributed Algorithms (Wednesday, October 10, 2012, 9:05): This talk describes a very high-level language for clear description of distributed algorithms and optimizations necessary for generating efficient implementations. The language supports high-level control flows where complex synchronization conditions can be expressed using high-level queries, especially logic quantifications, over message history sequences. Unfortunately, the programs would be extremely inefficient, including consuming unbounded memory, if executed straightforwardly.
We present new optimizations that automatically transform complex synchronization conditions into incremental updates of necessary auxiliary values as messages are sent and received. The core of the optimizations is the first general method for efficient implementation of logic quantifications. We have developed an operational semantics of the language, implemented a prototype of the compiler and the optimizations, and successfully used the language and implementation on a variety of important distributed algorithms.
A paper describing this work is at http://www.cs.stonybrook.edu/~liu/papers/DistPL-OOPSLA12.pdf (Joined work with Scott D. Stoller, Bo Lin, and Michael Gorbovitski)
A paper describing our work on high-level specifications is at http://www.cs.stonybrook.edu/~liu/papers/DistSpec-SSS12.pdf
I will also discuss important directions for future research.$ Fritz Henglein, A call for Algol 2020 (Wednesday, October 10, 2012, 10:52): The physical limitations of computing increasingly show themselves in established cost models such as the Random Access Machine no longer providing reliable predictions for scalability of program performance on large data quantities. We sketch why spatiality of computation, storage and communication needs to be modeled in computing models as a basis for adequate performance predictions on modern massively parallel computer hardware, and we argue that a spatially sensitive high-level abstract algorithmic programming model is required to develop efficient algorithms and render them as architecture-independent programs. $ Johan Jeuring, Inferring contracts (Thursday, October 11, 2012, 9:05): In Ask-Elle, our programming tutor for Haskell, students develop programs interactively and incrementally. When a student makes an error, we detect this via testing. We do not only want to report the error, but also the location of the error as precisely as possible. To determine the location of an error, we want to infer contracts for components of a student solution given the contract for the main function of the task. This talk motivates the idea, and discusses how you can approach it. $ Jules Desharnais, Some relational style laws of linear algebra (Thursday, October 11, 2012, 11:00): We present a few laws of linear algebra inspired by laws of relation algebra. The linear algebra laws are obtained from the relational ones by replacing union, intersection, composition and converse by the linear algebra operators of addition, Hadamard product, composition and transposition. Many of the modified expressions hold directly or with minor alterations. $ Hendrik Boom, Circumventing Gödel (Thursday, October 11, 2012, 12:03): No abstract provided. $ Bernhard Möller, Transitive separation logic (Thursday, October 11, 2012, 14:01): Separation logic (SL) is an extension of Hoare logic by operations and formulas that not only talk about program variables, but also about heap portions. Its general purpose is to enable more flexible reasoning about linked object/record structures. In the present paper we give an algebraic extension of SL at the data structure level. We define operations that additionally to heap separation make assumptions about the linking structure. Phenomena to be treated comprise reachability analysis, (absence of) sharing, cycle detection and preservation of substructures under destructive assignments. We demonstrate the practicality of this approach with the examples of in-place list-reversal and tree rotation. Moroever, we hint at how this might be extendded to more complex data structures such as doubly linked lists or threaded trees. $ Marc Frappier, Controller Synthesis Using Alloy (Thursday, October 11, 2012, 16:00): No abstract provided. $ Eric Hehner, Problems with the Halting Problem (Friday, October 12, 2012, 11:10): Last meeting I talked about Problems with the Halting Problem. While at Turing100 in Manchester in June, Ruurd Kuiper and Kees Huizing suggested that instead of starting with a "proof" of the halting problem and analyzing it, I might make my point better in reverse. Their suggestion worked well, so in this presentation I started with the essential inconsistency, and built the "proof". Slides are here. Eric also sang a song about the Halting Problem.
I've recently proposed a monadic-based notation for "distribution comprehensions" that includes filters that act to condition a distribution. It seems to work reasonably well, but I'd like to understand its structure better so that it can be extended.
The problem is this: what is mzero in the probability monad? I don't know. Can the group help?
|HaltingProblem.pdf||manage||200 K||09 Oct 2012 - 20:22||JohanJeuring|
|PHPOttawa.pdf||manage||83 K||13 Oct 2012 - 20:08||UnknownUser|
|RelationalStyleLawsOfLinearAlgebra.pdf||manage||246 K||14 Oct 2012 - 03:02||UnknownUser||Some Relational Style Laws of Linear Algebra|
|TheUnOfProgramming.pdf||manage||117 K||13 Oct 2012 - 08:40||JeremyGibbons||The Un of Programming (slides)|
|Voigtlaender.pdf||manage||438 K||10 Oct 2012 - 02:20||JohanJeuring|
|txt||WebCache.txt||manage||1 K||09 Oct 2012 - 18:04||JeremyGibbons|