WG 2.8 Estes Park, August 11-15, 2014

Monday AM

Wadler: Contracts and Unions: a demonstration
TypeScript TNG (Wadler grant from MS)

contracts:
manifest :  M: A =>p B     (p a blame label, positive (ascribed term blamed) or negative (context blamed))
latent:     M: Any =>p A =>p Any  ===  M @p A

e.g.  a type contract:  Int -> Int \/ Any -> String
    a function which could map Int to Int, or maybe it maps Any to String

---------------
Dan Licata (Wesleyan Univ)
Synthetic geometry
(homotopy type theory - a synthetic notion of spaces)
Univalence: equivalence of types is a generalization of bijection of sets

Robby Findler
Coq program for monad for reasoning about the runtime complexity of functions
Braun trees

Adam Chlipala
Functional Programming and World Domination (Coq)

Lunch

Ron Minsky
Code review

Matthias Felleisen
Networks all the way down

Norman Ramsey
Jumbo ML: Language Support for CS2

Matt Might
Deletion from Okasaki's Red-Black Trees: A Functional Pearl

---------
Tuesday

Programming Up-to-congruence, Again
Stephanie Weirich
Zombie language with dependent types
  hybrid of functional language and logic (allowing nontermination)
  logical fragment and programmatic fragment
  nontermination allowed in programmatic fragment only

Oleg Kiselyov
Lambda: the ultimate syntax-semantics interface
 [Haskell] linguistic application

Dimitriov Vytiniotis
What is ZIRIA: A 2-level language
  stream transforms and stream "computers"

Steve Zdancewic
Excape
 program synthesis in various problem domains
 - robotics control (synthesize plans)
 - cache coherence protocols
 - education (synthesize feedback based on buggy student code)

Lunch

Derek Dryer (Aaron Turon, Viktor Vafeiadis)
GPS: navigating weak memory with ghosts, protocols, and separation
  - concurrent program logics (based on separation logic)

Nate Foster
Deciding NetKAT ...
  - network programming languages (software defined networks)
  - NetKAT - functional language for describing packet processing

John Reppy
Compiling NESL to GPS

Jack Dennis
Programming Models for Massively Parallel Computation:
  The Chaotic State of the Art


Wednesday, afternoon

Eijiro Sumii
Normalizing Structured Graphs
 - structured graphs (Oliveira-Cook ICFP 12)
 - use recursive bindings and PHOAS (param. h-o. abstract syntax)
   to represent trees with sharing and cycles
 
  let rec x = a[x] in x  - cycle
  let y = a in b[y,y]    - sharing

 - structured graph reps are not unique, can be redundant
 - simplify and normalize representation terms
 - equivalence upto graph bisimilarity

Amal Ahmed
Fully Abstract Closure Conversion (in the presence of state and
effects)
  - verified compilers for a multi-language world
  - correct compilation of components (last meeting)
  - secure compilation of components (today's topic)

Fritz Henglein
Soundness is not Sufficient

Debate about the usefulness or importance of "soundness"
(e.g. of a type system, or of a statis analysis algorithm or tool)
Felleisen, Might

Thursday
--------

John Hughes
Finding more bugs and good examples with QuickCheck

Dave MacQueen
Early History of ML

Arvind
Processor specification without a memory model

Conal Elliot
Tabula
  space-time architecture (Minkowski space)
  tremendous flexibility for moving computations in space & time
  program in a non-sequential language: Haskell
  open compiler development
  compiling Haskell to Verilog (hardware description language)

Mark Jones
Optimization using Monadic intermediate language
  secure microkernel written in Habit

Lennart Augustsson
Report from the trenches, again
  Haskell at Chartered Standard Bank
  local version of Haskell: Mu
    strict
    no recursion
    string as a primitive type
  about 200 users, more Mu code than C++


Friday
------

Benjamin Pierce
The Spider Calculus


================================================================================
Attendees

Amal Ahmed (Northeastern)  
Arvind (MIT)   
Lenart Augustsson (Standard Chartered Bank)  
Adam Chlipala (MIT)  
Jack Dennis (MIT)  
Dereck Dreyer (MPI)  
Conal Elliot (Tabula)  
Robby Findler (Northwestern)
Matthias Felleisen (Northeastern)
Nate Foster (Cornell)  
Fritz Henglein (DIKU)  
John Hughes (Chalmers)  
Mark Jones (PSU)  
Oleg Kiselyov (Univ. of Tsukuba, Japan)  
Dan Licata (Wesleyan)  
David MacQueen (Chicago*)  
Matthew Might (Utah)  
Ron Minsky (Janes Street)   
Benjamine Pierce (Penn)  
Norman Ramsey (Tufts)  
John Reppy (Chicago)  
Mary Sheeren (Chalmers)  
Satnam Singh (Google)  
Eijiro Sumii (Tohoko Univ)  
Dimitrios Vytiniotis (MSR Cambridge)  
Phil Wadler (Edinburgh)  
Stephany Weirich (Penn)
Steve Zdancewic (Penn)

Denmark 1
Sweden 2
Britain 2
Germany 1
Japan 2
US 20