Ottawa

IFIP21
Main.TwoDotOneGroup, Main.TwoDotOneObserversGroup

%TOC%

---++ Minutes

---+++ Participants

   * Hendrik Boom
   * Jules Desharnais
   * Marc Frappier
   * Jeremy Gibbons
   * Rick Hehner (and Margaret)
   * Fritz Henglein
   * Ralf Hinze
   * [[http://www.chalmers.se/cse/EN/people/jansson-patrik][Patrik Jansson]]
   * Johan Jeuring
   * Annie Liu
   * Lambert Meertens
   * Bernhard M&ouml;ller
   * Carroll Morgan
   * Tom Schrijvers
   * Akimasa Morihata
   * Tarmo Uustalu
   * Janis Voigtl&auml;nder
   * Dave Wile (and Linn)

---+++ Organizational and administrative matters

Friday morning, October 11, 2012.

   $  _Membership_ : These private matters are not recorded in the public version of the minutes.

   $  _Formal resolution_ : The members of WG2.1 and the observers present at the 69th meeting in Ottawa wish to express their thanksgiving to Rick Hehner of the University of Toronto and to Margaret Jackson for organizing a wonderful meeting in this beautiful capital city. They even carefully specified the weather for the excursion<p> rain * oatdoors . <p> 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.<p>----------------------------------------------------------------------<p>Les membres du WG2.1 et les observateurs présents à la 69e réunion à Ottawa tiennent à exprimer leur Action de grâces envers Rick Hehner de l'Université de Toronto et à Margaret Jackson pour avoir organisé une réunion extraordinaire dans cette belle capitale. Ils ont même soigneusement spécifié le temps de l'excursion<p> pluie * grain' air .<p>Nous avons apprécié une étude approfondie des systèmes d'écriture hiéroglyphiques et d'autres notations complexes de calcul, que nous nous réjouissons de continuer à la prochaine réunion - à condition que le monde ne s'arrête pas le 23 Décembre 2012.

   $  _Algol 68_ : Via Paul <nop>McJones: With permission from IFIP, a link to a scanned copy of the final revision of Lindsey and van der Meulen's [[http://www.softwarepreservation.org/projects/ALGOL/standards/#ALGOL_68_informal_introduction][Informal Introduction to Algol 68]]. <p> There is a [[http://www.compileonline.com/execute_algol_online.php][website with an online version (an interpreter) of Algol 68 (Marcel van der Meer's Algol 68 Genie)]]. 

   $  _Next meetings_ : The 70th meeting will be held in Ulm, Germany, July  1 - 5, 2013, organised by Helmuth Partsch. The 71st meeting will probably be held somewhere in Europe. Robert Dewar proposes to organise a next meeting at his house, so this might be a possibility for the 72nd meeting.

   $ _Scheduling procedure_ : We have started with 10 minute uninterrupted introductions by all people who want to present a talk. 

This meeting is organized by Eric Hehner. 

---+++ Technical presentations in scheduled order

   $ Tarmo Uustalu, _Composing directed containers_ (Monday, October 8, 2012, 14:05): No abstract provided.

   $ Main.JeremyGibbons, _[[%ATTACHURL%/TheUnOfProgramming.pdf][The Un of Programming]]_ (Monday, October 8, 2012, 16:10): My continuing tale of reasoning with effectful functional programs. Previous episodes were presented in [[AtlanticCity]] and [[Rome]]; this episode is about reasoning about an effectful tree traversal, in terms of its inverse. !McBride and Paterson's _Traversable_ type class is almost what one wants, but not quite; I'll explain why, and why not.

   $ Tom Schrijvers, _[[%ATTACHURL%/ifip_mtc.pdf][Meta-Theory a la Carte]]_ (Tuesday, October 9, 2012, 9:05): Formalizing meta-theory, or proofs about programming languages, in a proof assistant has many well-known benefits. However, the considerable effort involved in mechanizing proofs has prevented it from becoming standard practice.  This cost can be amortized by reusing as much of an existing formalization as possible when building a new language or extending an existing one.  Unfortunately reuse of components is typically ad-hoc, with the language designer cutting and pasting existing definitions and proofs, and expending considerable effort to patch up the results.<p>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.<p>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 <p> A paper describing this work has recently been accepted at POPL 2013 [[http://users.ugent.be/~tschrijv/Research/papers/popl2013.pdf]].

   $ Janis Voigtl&auml;nder, _[[%ATTACHURL%/Voigtlaender.pdf][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ürneisen), 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 <nop>QuickCheck and/or <nop>SmallCheck.

   $ Patrik Jansson, _[[%ATTACHURL%/Feat_PJ.pdf][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 <nop>QuickCheck generators) and exhaustive enumeration (in the style of <nop>SmallCheck). For more details see http://wiki.portal.chalmers.se/cse/pmwiki.php/FP/Testing-Feat . (There is a [[http://dl.acm.org/citation.cfm?id=2364515&CFID=114228077&CFTOKEN=91363922][paper]] about this in the [[http://www.haskell.org/haskell-symposium/2012/][Haskell Symposium 2012]].)

   $ Ralf Hinze, _[[%ATTACHURL%/Hinze.pdf][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.<p>This is joint work with Daniel W.H. James, Thomas Harper, Nicolas Wu, José Pedro Magalhães.

   $ Akimasa Morihata, _[[%ATTACHURL%/morihata_ottawa.pdf][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.<p> 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. <p>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. <p>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. <p>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) <p>A paper describing our work on high-level specifications is at http://www.cs.stonybrook.edu/~liu/papers/DistSpec-SSS12.pdf <p>I will also discuss important directions for future research.

   $ Fritz Henglein, _[[%ATTACHURL%/A-call-for-Algol-2020.pdf][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, _[[%ATTACHURL%/InferringContracts.pdf][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, _[[%ATTACHURL%/RelationalStyleLawsOfLinearAlgebra.pdf][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&ouml;del_ (Thursday, October 11, 2012, 12:03): No abstract provided.

   $ Bernhard M&ouml;ller, _[[%ATTACHURL%/TransSepSliWG21.pdf][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 [[http://www.cs.utoronto.ca/~hehner/PHP.pdf][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 [[%ATTACHURL%/PHPOttawa.pdf][here]]. Eric also sang a [[%ATTACHURL%/The-Halting-Song.m4a][song]] about the Halting Problem.

---+++ Information about problems

   $ Carroll Morgan, _[[%ATTACHURL%/HaltingProblem.pdf][Notes on the Halting Problem]]_: A (short!) contribution to the Halting Problem which I put together while discussing the issue "over the ether" with Rick.

   $ Lambert Meertens, _[[%ATTACHURL%/WebCache.txt][A Web Cache]]_: A problem challenge about web caches.

   $ Carroll Morgan, _How do you do guards in the probability monad?_: In Wadler's "Comprehending Monads" (and recently revived in Giorgidze et al, 2011) it's shown how to have comprehensions for arbitrary monads. Well, almost arbitrary: if you want guards (aka filters) then your monad has to have a zero. In Haskell (-speak) that means it should be an instance of class <nop>MonadPlus, thus with a constant mzero that satisfies certain conditions.<p>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. <p>The problem is this: what is mzero in the probability monad? I don't know. Can the group help?

---++ Pictures from the meeting

   * [[%ATTACHURL%/Public1.zip][Carroll Morgan's pictures 1]]
   * [[%ATTACHURL%/Public2.zip][Carroll Morgan's pictures 2]]
   * [[%ATTACHURL%/Public3.zip][Carroll Morgan's pictures 3]]
   * [[%ATTACHURL%/Public4.zip][Carroll Morgan's pictures 4]]
   * [[%ATTACHURL%/Public5.zip][Carroll Morgan's pictures 5]]
   * [[%ATTACHURL%/Public6.zip][Carroll Morgan's pictures 6]]

---++ Meeting information

The meeting will be held in Ottawa, 2012 October 8 to 12.

---+++ Location

[[http://www.sheratonottawa.com][Sheraton Hotel]]<br>
150 Albert St.<br>
Ottawa ON <nop>K1P 5G2<br>
phone 1-613-238-1500<br>
fax 1-613-235-2723

From Ottawa International Airport (YOW), either

   * take bus 97, direction Bayshore, and get off at Albert St.  The buses run every 15 minutes, and take 28 minutes to get there, and cost $3.30 for a regular single fare, $2.00 for a senior (65+) single fare.
   * take a taxi for $30.  That's a 20 minute drive.

---+++Registration and accommodation

Rooms are reserved for us until September 7 at the daily rate $149 plus 13% tax for 1 or 2 people.  You can reserve by emailing reservations@sheratonottawa.com and identifying yourself as being part of the group "International Federation for Information Processing" or "IFIP".

checkin 15:00;  checkout 12:00

---+++Internet

The hotel bedrooms have free internet.  The meeting room has internet for only the chair and secretary.

---+++Latest information

---++Meeting programme
  
---+++Schedule

We will start at 9:00 on Monday and finish at noon on Friday. Please arrange to be there for the whole meeting.

Monday, Tuesday, and Thursday, the schedule is as follows:

   * session - 9:00 to 10:30
   * coffee break - 10:30 to 11:00
   * session - 11:00 to 12:30
   * lunch - 12:30 to 14:00
   * session - 14:00 to 16:00
   * coffee break at 16:00 to 16:30
   * session - 16:30 to 18:00

The meeting takes place in the Presidential Suite, which is on the top floor of the hotel.

---+++Excursion

The excursion will begin Wednesday at 14:00 at the Sheraton Hotel.  We will have a one hour bus tour of [[http://www.ottawatourism.ca/en/visitors/top-attractions][downtown Ottawa]] followed by a three hour visit to the [[http://www.civilization.ca/home][Museum of Civilization]].  Optionally, some of the time allocated to the museum may be spent at the [[http://www.gallery.ca/en/][National Gallery]].

---+++Concert

On Wednesday October 10 at 20:00, after the excursion, after you have had something
to eat, a guitarist I like very much, [[http://murielanderson.com][Muriel Anderson]], will be playing at [[http://lemichelange.ca/ottawa/index.html][Le Michel-Ange coffee house]].  Tickets are $20 each.  Please inform me hehner@cs.utoronto.ca immediately if you wish to go. For those going, I have reserved dinner at the [[http://http://www.parliamentpub.com][Parliament Pub]], Sparks St and Metcalfe St, at 18:00, and transportation from there at 19:15.

---+++Banquet

The banquet is Thursday at 18:30 at [[http://www.fairmont.com/laurier-ottawa/dining/wilfrids/][Wilfrid's Restaurant]] in the [[http://en.wikipedia.org/wiki/Château_Laurier][Chateau Laurier]].

---+++Cost

The cost per participant depends on the number of participants.  With the current small number of just 17, the cost is unfortunately high;  if anyone else drops out, it will go higher.  At present, in Canadian dollars (equal to American dollars), it looks like:
   * meeting room + breaks + lunches + equipment: $500
   * excursion: $40
   * concert: $20
   * banquet: $70
You can compute your total knowing how many of each item apply to you.  I have no means to accept credit cards.  You may pay cash or interac eTransfer.  For the former, there are ATMs, of course.  For the latter, you need only my email address (hehner@cs.utoronto.ca), and you make up a question to which I know the answer.  How about "What is the first name of our current chair?"?

-- Main.JeremyGibbons - 08 Oct 2012
Topic attachments
I	Attachment	Action	Size	Date	Who	Comment
pdf	HaltingProblem.pdf	manage	200.3 K	09 Oct 2012 - 20:22	JohanJeuring
pdf	PHPOttawa.pdf	manage	83.7 K	13 Oct 2012 - 20:08	EricHehner
pdf	RelationalStyleLawsOfLinearAlgebra.pdf	manage	246.3 K	14 Oct 2012 - 03:02	JulesDesharnais	Some Relational Style Laws of Linear Algebra
pdf	TheUnOfProgramming.pdf	manage	117.7 K	13 Oct 2012 - 08:40	JeremyGibbons	The Un of Programming (slides)
pdf	Voigtlaender.pdf	manage	438.2 K	10 Oct 2012 - 02:20	JohanJeuring
txt	WebCache.txt	manage	1.8 K	09 Oct 2012 - 18:04	JeremyGibbons