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 (and they will...). 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.
Invited and informal talks, workshop presentations, lectures and
seminars, with the slides, are listed below. Conference talks are in
the proceedings section.
Programming and Proving with Distributed Protocols [Slides]
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]
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
Concurrency Yak at POPL 2014. San Diego, CA, USA.
Monadic Abstract Interpreters
Invited talk at 15th International Symposium on
Principles and Practice of Declarative Programming (PPDP 2013). Madird, Spain.
Static Analysis and Code Optimizations in Glasgow Haskell
[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
Devoxx 2008. Antwerp, Belgium. December 2008.