Lambda the Ultimate

That could be quite interesting to discuss. You never really know till you try, of course; sometimes a promising topic just doesn't spark; but it seems to me to have some potential.

I like the historical perspective, and the way that it ties neatly into (many) views of what is interesting right now.

Somebody really needs to volunteer to become a PLT historian, but most of us are too busy chasing our pink elephants to bother.

Perhaps this could be broken up over several topics, each of which contains a brief bibliography of materials available on-line.

For example, for lisp: early papers; papers typical of what they were reacting to; some noteworthy retrospective papers.

It might be too much to ask but a pie-in-the-sky wish would be for this to result in a big pile of PDFs that can be free shared.

I'm putting this here because it might fit as one specific sub-branch looking at how Haskell has changed between 1998 and 2010. It seems hard to pin down a specific point in time, but some (very vague) trends would be:
* Monads were once an 'exotic' topic. Literally at the back of the textbook that we had as undergrads. Now a monad transformer stacks seems to be the standard approach to any non-pure problem.
* Hitting the limits of expressibility in universal types, particular in domains that language hackers care about: i.e writing interpreters and compilers.
* The number of "Haskells" seems to have multiplied because many language extensions seem to have become necessary for different domain problems.
* Ten years ago there were interesting research directions around SYB on one hand, and tagless interpreters on the other. Where did it go next?
I'm writing this because sitting down to write an interpreter in Haskell for the first time in about a decade I'm quite shocked by how much it has changed. I'm wondering what happened to the research direction of how to handle the genericity of ASTs cleanly within Haskell. Did it reach a definite ending point as a solved problem (and if so where is the best place to look for a tutorial on how to do it) or did it just sort of peter out as reaching a state that was "good enough" that people moved on to other things? Roughly speaking this could be one strand within "good stuff at ICFP and other venues" over the years in question.

Those things are still being researched. The main change in Haskell the language seems to be its convergence toward dependent types (driven, in part, by typed interpreters -> GADTs). In the community things that were once hard are now ordinary. This is how it goes with many topics. Things that were at the top of mathematics and physics achievements not so long ago are now taught in undergraduate mathematics and physics. Even in programming I've heard that this happened: long ago OOP was like monads; thought to be hard and exotic and only known to experts.

Here are some major advances in semantics, from about 1980 to about 2000. I'll stop there because the list is already getting long....

• Rely/guarantee reasoning: 1981
• The effective topos: 1982
• Reynolds' parametricity: 1983
• Girard's linear logic: 1987
• Wadler and Blott's typeclasses: 1989
• PER models of System F: 1990
• Moggi's monadic semantics of effects: 1991
• Wright/Felleisen syntactic type soundness: 1994
• Proof-carrying code: 1996
• O'Hearn and Reynolds' Separation logic: 1999
• Step-indexed logical relations: 2001

This is a very partial list: I've left out a lot of stuff, such as denotational advances like the application of categorical methods to domain theory, game semantics, advances in proof theory like focalization, anything to do with concurrency and pi-calculus, and anything to do with model checking or SMT, and anything to do with implementation (whether of model checkers, compilers, or proof assistants).

Anyway, IMO the real excitement doesn't come from any single advance. It comes from the fact that enough knowledge has been built up that we can actually cash the checks that verification/semantics wrote in the 1970s -- completely correct system software, with machine-checked proofs all the way from specs to machine code, is now feasible to build. Milner, Hoare, Djikstra and co. were right, and we can prove it.

So where is my commercially viable fully formally specified and checked operation system? And where is my hover board, it's 2015 already!

So where is my commercially viable fully formally specified and checked operation system?

seL4!

My answer is a bit tongue-in-cheek, but I could not resist. It is true that seL4 is only a kernel, and would probably not run as is on computers you are interested in. On the other hand, it was successfully transferred to the industry and eventually found its way into a bunch of phones, if I remember correctly. It's a tangible proof that, at least in some contexts, formally verified software is feasible and useful.

And where is my hover board, it's 2015 already!

Science takes time.

The question: Which one?

From Lexus:
http://www.people.com/article/hoverboard-real-back-to-the-future

or Hendo: http://www.digitaltrends.com/cool-tech/hendo-hover-board-kickstarter-back-to-the-future/

:-)

Heiko

I really like this list, thanks!

Looking at the accepted paper list...wow. They are up there with PLDI and OOPSLA.

1. A Scalable, Correct Time-Stamped Stack
2. From Communicating Machines to Graphical Choreographies
3. Equations, contractions, and unique solutions
4. Formal verification of a C static analyzer
5. Space-Efficient Manifest Contracts
6. Quantitative Interprocedural Analysis
7. Integrating Linear and Dependent Types
8. Functors are type refinement systems
9. Safe and Efficient Gradual Typing for TypeScript
10. Sound Modular Verification of C Code Executing in an Unverified Context
11. Program Boosting: Program Synthesis via Crowd-Sourcing
12. Programming up to Congruence
13. Deep Specifications and Certified Abstraction Layers
14. A Meta Lambda Calculus with Cross-Level Computation
15. Specification Inference Using Context-Free Language Reachability
16. Runtime enforcement of security policies on black box reactive programs
17. Faster Algorithms for Algebraic Path Properties in RSMs with Constant Treewidth
18. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
19. DReX: A Declarative Language for Efficiently Computable Regular String Transformations
20. K-Java: A Complete Semantics of Java
21. Higher Inductive Types as Homotopy-Initial Algebras
22. A Calculus for Relaxed Memory
23. Compositional CompCert
24. Abstract Symbolic Automata
25. Analyzing Program Analyses
26. Self-Representation in Girard's System U
27. Conjugate Hylomorphisms: The Mother of All Structured Recursion Schemes
28. Decentralizing SDN Policies
29. Polymorphic Functions with Set-Theoretic Types. Part 2: Local Type Inference and Type Reconstruction
30. Principal Type Schemes for Gradual Programs
31. Full Abstraction for Signal Flow Graphs
32. Dependent Information Flow Types
33. Common compiler optimisations are invalid in the C11 memory model and what we can do about it
34. Manifest Contracts for Datatypes
35. Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks
36. Leveraging Weighted Automata to Compositional Reasoning of Probabilistic Programs
37. Algebraic effects linearity and quantum programming languages
38. Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
39. Probabilistic Termination
40. Tractable Refinement Checking for Concurrent Objects
41. From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification
42. Ur/Web: A Simple Model for Programming the Web
43. Differential Privacy: Now it's Getting Personal
44. Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant
45. Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests
46. Succinct Representation of Concurrent Trace Sets
47. Predicting Program Properties from Big Code
48. On Characterizing the Data Access Complexity of Programs
49. A Coalgebraic Decision Procedure for NetKAT
50. Proof Spaces for Unbounded Parallelism
51. Towards the Essence of Hygiene
52. Data Parallel String Manipulating Programs

I can't see anything that suggests a topic changes or an emerging hot topic, but POPL isn't my thing.

Topics that were big at POPL this year:

* Verified compiler correctness/compilation to relaxed memory
* Gradual typing/dynamic languages
* SDNs
* Program synthesis
* Big semantics

This is, of course, a subset of "what's hot in academic PL in the last 5 years".