Wednesday January 11th
POPL Day 2
Notes from POPL Day 2
Keynote
Type Soundness Theorem  Derek Dreyer
 Rob Milner: Theory of Type Polymorphism in Programming “welltyped programs cannot go wrong”
 Andrew Wright, Matthias
“syntactic approach to type soundness”
 welltyped programs can’t get stuck
 Progress and Preservation
 Progress: future state or valid terminal state
 Preservation
 Limits:
 Limit 1: Data Abstraction
 Limit 2: Unsafe Features: See “Prepooping your pants with Rust (Alexis Beingessner, Leakpocalypse)
 Landmark Semantic Soundness
 Milner (1978): used a “logicalrelations” model based on denotational semantics. Didn’t scale to richer type systems (eg. ML)
 Appel, McAllester (2001): introduced a “stepindexed” logicalrelations model of recursive types using operational semantics
 Ahmed (2004) : Scaled “stepindexed” model to handle higherorder state using recursive Kripke structures
 Iris  implement in Coq system
 HigherOrder Hoare Logic : If P holds initially, then e is safe to excecute. Bind Rule
 Iris’s Monadic Bind Blue
 Separation Logic
 Concurrent Separation Logic
 Perfect for modelling concurrent languages with substructural type systems like Rust
 Persistent vs Ephemeral
 Ephemeral: value can change: we assume a type, but may change as we step through programme
 Proving that ADT is semantically welltyped
 Ghoststate: logical state in proof but not physical state in programme
 PCM: partial commutative monad Takeaway: Good type systems support data abstraction and safe encapsulation of unsafe features
Linear Haskell
( This talk was OK: I wish it were longer, more detailed, and the points not as trivialized) ( Intersestingly, my friend, Ben, also agreed with me).
 Higher Order Constrained Horn Clauses for Verification
 Jones: Optimal Partial Evaluation
 Wadler: Linear Types
 Linear types seem to require deep changes to the language
f::A>B
 If f U is consumed exactly once, then U is consumed exactly once
 Polymorphic foldl instead of linear foldl
 Linearity Polymorphism (no subtyping)
Polyvariadic Approximations: Fibrations and Intersection Types
(This was definitely not clear to me, so the notes are very shortended.)
 Calculus as Catoperands
 a 2morphism between multimorphisms is a cutelimination path
 Approximate presheaf: An approximate on MELL defines the approximation presheaf
 The Groethendieck construction: subject reduction: subject reduction/ subject expansion
 The fundamental theorem of intersection types (Mazza, Pellisier, Vial)
 If A compose G have properties relative to
 a family of Reductions R_s
 a strategy R_w
 then we can go from a weak to a strong type (I drew the diagram for this)
 CoppoDezani idempotent type system
 de Carvalho’s System R
 KesnerVial’s system for the lambda u  calculus and gets their normalization properties and reduction strategies
Unifying Analytic and Statically Typed Quasiquotes
 Analytic Quasiquotes  code as data
(I’ve heard of code as data in Clojure.spec, but not familiar with quasiquotes)
 Staticallytyped quasiquotes
Lunch Break :D
 I was actually in peopleoverload so I ended up taking a two hour nap in a quiet room.
Safety and Conservativity for HOL and Isabelle / HOL (Andrei Popescu)
 Implementation bug eg side condition of inference rule not implemented correctly (Conceptual)
 logical flaw eg termination/ guardedness checker (Logical)
 Maxime Denes and Daniel Schepler (bug allowed inconsistency axiomatic extensionality)
 Isabelle: Ondrej Kuncar (2014)
 2 approaches to theorem proving:
 Axiomatic (unsafe)
 Definitional (safer but less convenient)
 Definitions can be compiled awa without loss of provability
 Proof Assistance: Definitional Ambitions
 Type Theory (Agda, Coq, Lean, Matita)
 Safer Provers (HOL> Higher Order Logic)
 Sacrifice Dependent Types (HOL4, HOL Light, Zero, Isabelle)
 all recursion reduced to nonrecursive definitions
 HOL Logic: Rank1 Polymorphic Classical HigherOrder Logic with Choice and Infinity

Typedefs introduce isomorphic copies (and are accepted only if the predicate is proven empty)
 Related Work: Wiedijk’s Stateless HOL, Barra’s Coq
Univalent Higher Categories via Complete Segal Types
(this was a highly interesting talk! I would love to read more about this!)
 I hadn’t heard of Segal Types before!
 Maclane’s Pentagon (I drew a diagram here). Basically you shift brackets to get from one composition to another
 AhrensKapulkinShulman (2015): categories where morphisms satisfy UIP
 A definition for higher categories in type theory: Complete semiSegal Types

 Semisimplicial types (give raw data)

 Segal condition (Rezk 2001) gives coherent composition

 Completeness (Lurie 2009/ Harpaz 2015), gives identity structure which moreover is univalent (different notions of obchecks coincide)


Identities: present trouble in type theory because of degeneracy and semisimplicial types
 Semisimplicial types
 type A_0 of points for any pair of points, we have type of lines
 for any “empty triangle”, a type of fillers (I have diagrams of these :D) (at this point, I also drew differences he demonstrated between Categories and Semisimplicial types)
 Segal condition (he demonstrated pentagon equality where the number of points is four so k = 4)
 he demonstrated that if the horns of the form are vectors in different directions, the form is neutral
 A semisimplicial type is complete if every point has exactly one outgoing neutral edge
 complete semiSegal ntype is a semisimplicial type (A_0, …, A_n+2 that satisfies:
 Segal condition
 completeness
 truncation (highest level trivial).
 (we rever to these three as propositions)
And..Posters
 I took photos of ones I found personally interesting.
 Zeina and Ben’s poster (Ben’s a Racketeer!)
 This was really interesting, and was done by a student I was able to speak with from MIT CSAIL where he was using Probabilistic Programming and Locale theory.
 He made a great analogy of a case where you flip a coin and want to get a head. However, over a sequence of tries, you could have a case where you never obtain one, and that creates a bit of an issue when dealing with probability (just that one case).
 This was pretty neat! Reminded me a lot of the process for say, machinelearning and driverless cars (where you are using probability and targets to train models).
 You can see how the function traverses the tree (left and right node), and where the end of the tree is, as it recurses upwards. And I don’t even use/read Anglican!
 This was over my head.
We had a banquet
 Later, we went over to MOCA and had a banquet. It was interesting for me, because I had a moment to speak with both the ACM Chair and my Student Volunteer Captain (who flew in from Edinburgh).
 Both were very interested in helping me, and had a heart to heart, and encouraged me very much to apply to ICFP, and offered a realistic path to doing my Master’s.
 I have to say, I’ve never met such a bunch of people who had so much faith in me. Everyone there seems to think I have some kind of great future. That’s really encouraging. And I’ve never quite “fit” with a group the way I do with these people. It felt great and I legitimately have looked forward to every single day of this conference.
 The next event I’m looking forward to is the CoqPL workshop on Saturday.
 There was also a publisher of technical books there, and I had to stop by his booth by the moment I saw it. We ended up chatting and he gave me his information and told me that he’s actually giving away the books displayed to student volunteers, and that I’m more than welcome to take the one I want.
So…
 It’s something I’m legitimately thinking about, because I honestly am not quite happy with the sort of opportunities with my level of experience, and would like an opportunity to do more research work in general.
 I’ve been thinking about whether it is worth it for me to put up with abuse, sexism, being treated like I am an absolute idiot, and all the other great things (sarcasm) that come as territory in joining the lower levels of the industry, and whether it is worth it, or if I’d be happier spending some time strengthening my technical skills and in working on projects I find interesting, going in also with a better skillset (or not at all, but I’d have the choice).
 I have other friends who really love web development, and I just don’t fit…at all.
 I have no desire to be a web developer, so I’m not in a rush to obtain that kind of job, or to join the tech world in general. But I want to do interesting work.
 I’ve been to all sorts of conferences, and I have to say, the ones I’ve found most enjoyable are the ones like these, or say, LambdaConf. I also like the people in those communities a lot, and they tend to be a lot more focused on quality and mentorship, which is important to me.
 No one at POPL cared much about where anyone works (which is common at a lot of confs); they all cared more about what people were working on. I liked that a lot. They wanted to make connections with people doing similar work.
However

Who knows how this will turn out? I have spoken to a few individuals in similar paths, and they’ve said that Apparently, unknowingly, a lot of what I’ve been doing lines up perfectly with this path. One that can include topics like probability / statistics, verification and a deeper understanding of things like type theory. So that’s certainly interesting.

Anyways, that’s it for now. Oh, I also got rejected by a company, but no worries because after last night’s conversations, it probably would not have been a good fit, in any case (lol).

So maybe I sound like I’m a little mixed up right now, but it’s OK. It’s good to be thoughtful and conscientious.
I trained a machine learning model
 Used svm.
 This is varying the kernel filter (linear vs rbf) and sample size to influence accuracy, and also find values at particular points