Saturday January 13th
Last Day of POPL
Closing

Today was the last day of POPL. It has been a lifechanging experience for me.

I have to say that being in LA has been tough for me, because there are few places where I’ve felt like the people believed in me, and treated me like an intelligent person. This was one such place. It’s been a while since I have felt like I could make an offhanded sarcastic comment, and people would ‘get it’, and where we shared a similar sense of humour. Antal even had a “Ithaca is Gorges” tshirt, which was immediately a talking point for both of us (I had no idea he was from Ithaca, and I lived there!). I haven’t had much in common locally in a long while, and even though these people were from all over the world, it was a real treat to just be able to talk about similar things, joke around and just have the best time. It was really a special week for me. It will miss the wit and intelligence and good humour of everyone.
 I made so many friends, had so many great times and learned so much, it was pretty much perfection. It’s a bit sad that it’s all over now. Or maybe it is just the beginning…

I had a conversation with W. Byrd today, and he told me to keep in touch. He told me about his path to Computer Science, which was really inspiring, and he told me that it isn’t about where you start, because he’s met lots of people who clock in and clock out, but it’s about having and sustaining that love, which he’s always had. I agree 100%. I also met the famous Fare and sat in on Stephanie’s talk!
 I’ve also been informed that OPLSS is having three weeks instead of two, and that you have to choose two. So one will be intro and intermediate, and another will be intermediate and advanced. Sounds great and I am looking forward to applying!
Notes CoqPL and some others
CoqHammer: Strong Automation for Program Verification
 Hammer goal: provide efficient facts from a large library.
 Hammers: work in three phrases
 premise selection (using ML)
 translation (selected lemmas)
 prove conjecture in logic of ITP
 evaluation:
 HOL(y) Hammer
 flyspeck text formalization (47%)
 similar results for HOL4
 slightly weaker for Cake ML

Concrete Semantics (Nipkow, Klein)
 Two machinelearning filters:
 K NN and Naive Bayes
 used for ML part
 Features F(T) of theorem T
 Variable P : nat > Prop
 T = forall k, l between k l > k <= l
 F(T) = Nat or Peano numbers
 D(T) dependencies
 Target logic: untyped FOL (first order logic) with equality
 for closed type tau = Product(x): alpha . beta(x), we have:
 G (tau, f) = forall x. G (alpha, x) > G (beta (x), f x)
 Overall Hammer evaluation
 all statements from Coq standard library
 ATP success 5%
 ATP used: E, 23
 Vampire w/ 30 seconds time limit
 Overall success 40.8%
 8 threads with different lemma selection, formalization, etc
 improvements needed for dependent types and boolean reflection
A Destruct Tactic for MTac (J. Kaiser)
 destruct  in Coq today
b : bool
H : b not equal true
b = false
 What happens
lambda (b : bool) (H : b not equal true), ? G : b = false where ? G is hole, what we need to prove
 destruct: call match w/ return type which mentions assumption
 Dependent Pattern Matching
 Mtac typed tactic language for Coq
 offers primitives for metaprogramming
 Typed Metaprogramming in Mtac element in list
 Definition inlist A(x:A): forall l :
 list A, M(In x l):= …
 Tactics in MTac
 Inductive goal : Type :=

Goal { G :Type} : G > goal 
Definition tactic :Type:= goal > list goal
 Mtac’s destruct is implemented entirely w/ dynamic types (not good)

new destruct tactic for Mtac guided by types
 Dependent Inductive Types
 Inductive vec (X: Type) : nat > Type:=

vnil: vec X 0 
vcons (x: X) {n} : vec Xn > vecX(Sn)  Representing Inductive Types
 Inductive T : forall i… i_k, Type : = …
 Future work:
 extend tactic power
 investigate performance
 test system w/ weirder inductive types
 replace all telescope types by more general version
Type Templated Coq (M. Sozeau)
 quoting and unquoting of terms and declarations
 compile: Ast term > Compcert.syntax
 standard binary parametricy
 uniform propositions
 similar MetCoq’s monad (shallow vs deep terms)
 http://templatecoq.github.io/templatecoq
Elpi (E Tassi)
 Embedded Lambda Prolog Interpreter
 Written in OCaml, designed as a library
 Extends lambda Prolog w/ constraints, modes…
 Lambda Prolog..
 Lambdatree syntax (HOAS): (x \ x) > identity function
 http://goo.gl/r6Nsja
Coqatoo (A. Bedford)
 I really enjoyed this talk! Great project!
 github.com/andrewbedford/coqatoo
 java application (coqatoo jar).
 you input coq file and select output mode (eg text)
 Step 1:
 information extraction
 proof tree construction
 Step 2: Number of subgoals:
 number of subgoals: if increases, node is branch, otherwise is leaf in tree
 Step 3: Tactic based rewriting
 limitation : we may not have all details
 Supports proofs in English or French
 Work done by Coscoy et all in the 90s was work done but used proofs from lambda terms inside of proof instead of tactic based rewriting
 Advantages:
 easy to control size and verbosity (one or two sentences per tactic).
 maintains order and structure of user’s original proof (not necessarily case in Coscoy)
 Disadvantages:
 only works on proofs whose tactics are supported while Coscoy’s worked on any proof
 won’t work well if there is a lot of automation
PureScript Group
 I hopped online to hang out with the PureScript group for 40 minutes
 Looked at updates from Documentation and Pursuit for PureScript
 Oath project > github.com/chexxor/purescriptoath
 spoke about differences between public and confidential oath
 was talking about JS and try catch asynchronous errors
 github.com/slamdata/purescriptaff/issues/136
 error channel can throw undefined actions on error channel
 so thinking of idiomatic node.js to idiomatic purescript
 fpcomplete.com/blog/2016/11/exceptionsbestpracticeshaskell (talking about how Haskell deals with errors)
 https://github.com/vladciobanu/purescripthalogenexample
Locally Nameless at Scale (S. Weirich)
 all Coq proofs (http://github.com/sweirich/corespec.git)
 errors in prior versions of the system pointed out in Eisenberg’s dissertation
 Curry style vs Church style type systems
 Church: Decidable, explicit, type annotations
 Curry: computationally relevant
D vs GHS
Gamma = a : A Gamma  a : A
Gamma = null o k gAMMA  null ok
 Tools used > Peter Sewell, Zappa, Nardelli et al
 Ott source file
 Tool based formalization
 Ott to coq language defs, Ott to syntactic lemmas, Ott to latex macros to paper sources
 coq language defs and syntactic lemmas to Coq proofs
 Ott: Locally Nameless Syntax
 Ott : Generated Definitions
 free and bound variables, substitutions and “dangling” bound variables
 Cofinite Quantification
 Ngen(Aydemir) gave lemmas for reasoning about lambda terms
 confluence > consistency in system (TaitMartin Lof, Barendregt, 1984)
 Irrelevant arguments, coercion
A Coq Formalization of R
 github.com/Mboin/proveR
Coq Panel
 Coq 8.7
 new features : cumulative inductive typees
 Coq users meeting
 Coq stack exchange (does this really exist?)
Phantom Types for Quantum Programs (R. Rand)
 Quantum programming and verification in QWuire
 Phantom Matrices
 Phantom Circuits
 Kronecker product multiplies dimensions
 Linear Types (https://github.com/jpaykin/QWIRE)
Param Coq
 Parametricity (Abishek)
 paramcoq (Keller and Larson)
Fare
 https://j.mp/FarePhD
Towards a System Approach to Distributed Programming (C. Meiklejohn)
 LASP
 Mentioned PPDP
I have to get up
 early in the morning to go whale watching, so I guess that’s it for me.
 But I have a lot to think about, and a lot to do moving forward.