CSL Family Tree
With the recently increased interest in the CS community to
concurrency verification, this slide, which I’ve
made sometime ago and which depicts the “flow of ideas” between modern
concurrency logics, became very popular, so I decided to put it online
for anyone who might want to use it in a presentation. I will keep it
updated with more logics to come. Feel free to drop me a line if you
need the diagram’s sources or want me to add your favourite logic,
which is missing.
Update: The CSL Family Tree depiction is now featured in the
Wikipedia article on Interference freedom (courtesy
of David Gries).
Talks
Invited and informal talks, workshop presentations, lectures and
seminars, with the slides, are listed below. Slides for conference
talks are available in the publications page.
-
Deductive Synthesis of Programs with Pointers: Expressive, Trustworthy, Fast [Slides]
-
CoSplit: Practical Smart Contract Sharding with Static Program Analysis [Slides]
-
Cardinality Analysis for Haskell Programs [Slides]
-
Chalmers University, Sweden, March 2021
-
The Scilla Journey:
From Proof General to Thousands of Nodes [Slides]
-
ICFP Programming Contest 2019 Report [Slides]
-
Functional Programming is Everywhere [Slides (PLMW@ICFP19)]
-
Engineering Distributed Systems that We Can Trust (and also Run) [Slides]
-
PODC 2019, Keynote talk, Toronto, Canada, August 2019
-
Composing Software Systems that are Provably Correct [Slides]
-
ECOOP 2019, Dahl-Nygaard prize keynote talk, London, UK, July 2019
-
Compositional Static Race Detection at Scale, without False Positives [Slides]
-
JetBrains, St. Petersburg, Russia, July 2019
-
National University of Singapore, April 2019
-
How to Bootstrap a Research Project [Slides (PLMW@POPL19)]
-
What We Talk about When We Talk about Formally Verified Systems [Slides]
-
Safe Smart Contract Programming with Scilla [Slides]
-
Deductive Synthesis of Programs that Alter Data Structures [Slides]
-
Aarhus University, Denmark, December 2018
-
National University of Singapore, November 2018
-
Imperial College London, UK, October 2018
-
KU Leuven, Belgium, September 2018
-
Inria Paris, France, September 2018
-
KAIST, Daejeon, Korea, August 2018
-
Distributed Consensus Protocols and Their Applications
[Lecture 1 |
Lecture 2 |
Lecture 3]
-
Scilla: Foundations for Verifiable Decentralised Computations on a Blockchain [Slides]
-
The Blockchain Connector, London Blockchain Developer Meetup, London, UK, May 2018
-
PLEMM 2018: Programming Language Enthusiasts Mind Melt, Bellevue,
WA, US, May 2018
-
University of California San Diego, CA, US, May 2018
-
Mechanising Blockchain Consensus [Slides]
-
University of Utah, UT, US, May 2018
-
Programming and Proving with Distributed Protocols [Slides]
-
University Paris Diderot – Paris 7, France, April 2018
-
Microsoft Research, Cambridge, UK, November 2017
-
National University of Singapore, October 2017
-
Heriot-Watt University, UK, July 2017
-
IMDEA Software Institute, Spain, June 2017
-
Aarhus University, Denmark, May 2017
-
University of California San Diego, USA, May 2017
-
Imperial College London, UK, November 2016
-
Guarding a Gallery with Sleepy Robots [Slides]
-
University of California San Diego, USA, February 2019
-
Yale-NUS College, Singapore, October 2017
-
Dependent Types for Verification of Real-World Programs [Slides]
-
Programming and Proving with Concurrent Resources [Slides]
-
University of York, UK, October 2016
-
University of Cambridge, UK, June 2016
-
Aarhus University, Denmark, June 2016
-
Max Planck Institute for Software Systems, Germany, May 2016
-
Imperial College London, UK, May 2016
-
Middlesex University, UK, May 2016
-
University of Birmingham, UK, January 2016
-
Queen Mary University of London, UK, December 2015
-
University College London, UK, April 2015
-
Microsoft Research, Cambridge, UK, March 2015
-
Reasoning about non-linearizable concurrent objects
-
Dagstuhl Seminar 16201, Germany, May 2016
-
University of Kent, UK, April 2016
-
Anatomy of mechanized reasoning about fine-grained concurrency
Dagstuhl Seminar 15191 on Compositional Verification Methods for
Next-Generation Concurrency, Schloss Dagstuhl, Germany, May 2015 [Slides]
-
Programming with Proofs
Google, London, UK. April 2015.
-
Towards Structured Mechanized Verification of Fine-Grained Concurrent Programs
The First International Workshop on Coq for PL at POPL 2015. Mumbai, India. January 2015.
-
Formal Mathematics as a Branch of Computer Science
Sociological Institute of the Russian Academy of Sciences, Saint
Petersburg, Russia. August 2014.
-
Communicating State Transition Systems for Fine-Grained Concurrent Resources
-
1st Microsoft Research and IMDEA Software
Institute Collaboration Workshop (MICW 2014). Madrid, Spain.
April 2014. [Slides]
-
2nd ACM SIGPLAN Workshop on
Higher-Order Programming with Effects (HOPE
2013). Boston, MA, USA.
September 2013. [Slides]
-
State Transition System alternative to Linearizability
[Slides]
Concurrency Yak at POPL 2014. San Diego, CA, USA.
January 2014.
-
Monadic Abstract Interpreters
Invited talk at 15th International Symposium on
Principles and Practice of Declarative Programming (PPDP 2013). Madird, Spain.
September 2013.
-
Static Analysis and Code Optimizations in Glasgow Haskell
Compiler
[Slides | SlideShare | Video]
SPb Functional Programming meetup. Saint Petersburg, Russia. December 2012.
- Dominance in Program Semantics, Dominance as Program Semantics
IMDEA Software Institute, Madrid, Spain. August 2012.
- Gradual Ownership Types
Entropy Meeting, Programming Languages Group,
Aarhus University. Aarhus, Denmark. December 2011.
- Scripting an IDE for DSL awareness
Devoxx 2009. Antwerp, Belgium. November 2009.
- Clojure support in IntelliJ IDEA
The Bay Area Clojure User Group meetup. San Francisco, CA, USA. June 2009.
- Cross-Language Development in IntelliJ IDEA
JAX 2009. Mainz, Germany. April 2009.
- Cross-Language Development Experience on the JVM
[Video]
Devoxx 2008. Antwerp, Belgium. December 2008.