Previous talks 2019-2016
title: “Meetings archive 2019-2014” draft: false weight: 3 displaythetitle: true
Seminar, Fall 2019
We meet every Monday from 13:00 until 15:00 in Nygaard-395. This meeting is organized by Danil Annenkov.
| Date | Who | Topic |
|---|---|---|
| September 9, 2019 | Jeppe Blaabjerg | Epistemic Modal Logic and non-interference (abstract) |
| September 16, 2019 | Aïna Linn Georges | Mechanisation of a capability machine and logical relations in Iris (abstract) |
| September 18, 2019, 11:00-12:00, Nygaard 295 | Andreas Nuyts | Dependent type theory with modalities, modes, and a right adjoint to the ∏-type (abstract) |
| September 23, 2019 | Alex Kavvos | Dr Levy: or How I Learned to Stop Worrying and Love Effects (abstract) |
| September 30, 2019 | Mario Alvarez-Picallo | From incremental computation to higher categories (abstract) |
| October 7, 2019 | Benedikt Ahrens | Initial semantics (abstract) |
| October 10, 2019, 16:15-17:00, in Aud. D3 (1531-215) | Paige North | Directed type theory and homotopy theory (abstract) |
| October 14, 2019 | No seminar - fall break | |
| October 21, 13:00-14:00, 2019 | David Naumann | Data Abstraction and Relational Program Logic (abstract) |
| October 22, 13:00-14:00 2019 | Simon Wimmer, TU Munich | Munta: A Verified Model Checker for Timed Automata (abstract) |
| October 28, 2019 | No seminar - Iris workshop | |
| November 4, 2019 | Matthieu Sozeau | Coq Coq Correct: Verification of Type Checking and Erasure for Coq, in Coq (abstract) |
| November 11, 2019 | Danil Annenkov | Verification of functional smart contracts in Coq (abstract) |
| November 13, 2019, 9:00-10:00 | Marieke Huisman | Automated Verification of Parallel Nested DFS (abstract) |
| November 13, 2019, 10:00-11:00 | Bart Jacobs | Specifying and verifying liveness properties of the I/O behavior of programs in separation logic (abstract) |
| November 18, 2019 | Jakob Botsch Nielsen | Smart Contract Interactions in Coq (abstract) |
| November 25, 2019, 13:00-14:00 | Thomas Van Strydonck | Linear Capabilities for Fully Abstract Compilation of Separation-Logic-Verified Code (abstract) |
| December 2, 2019 | Sabine Oechsner | Modelling security - A cryptographer’s view of the world (abstract) |
| December 9, 2019 | Karl Palmskog | mCoq: Mutation Analysis of Verification Projects (abstract) |
| December 16, 2019 | Zesen Qiang | A hands-on tutorial on cubical Agda (abstract) |
Seminar, Summer 2019
We meet every Monday from 13:00 until 15:00 in Nygaard-295. This meeting is organized by Kristoffer Just Arndal Andersen. The list of previous seminars is available here.
| Date | Who | Topic |
|---|---|---|
| May 6, 2019 | Alix | Compiler Correctness, Verification & Secure Compilation |
| May 27, 2019 | Martin | TYPES Practice: Coherence via big CwF of LCCCs |
| June 3, 2019 | Jakob Van Raumer (Nottingham) | Path Spaces in Homotopy Coequalizers |
| August 21, 2019, 10:30 | Jaco van de Pol | Parallel SCC Algorithms for Model Checking (CONCUR+FMICS invited lecture) |
| August 27, 2019, 12:00 – 13:00 in Nygaard-295 | Reza Sefidgar (ETHZ) | Formalizing Constructive Cryptography using CryptHOL |
| August 28, 2019, 15:00 – 16:00 in Nygaard-295 | Kenji Maillard (INRIA) | Towards program verification for arbitrary monadic effects |
| August 29, 2019, 14:30 – 15:30 in Nygaard-295 | Thomas Sibut-Pinot | TBA |
Seminars, Spring 2019
| Date | Who | Topic |
|---|---|---|
| Jan 7, 2019 | Søren & Bas | |
| Mathias | POPL Practice Talks | |
| Danny | ||
| Kristoffer | ||
| Jan 14, 2019 | - | POPL Week |
| Jan 21, 2019 | Kristoffer | Distributed Protocol Combinators |
| Jan 28, 2019 | Jaco | Identities and Inequalities for Fixpoint Equation Systems |
| Feb 4, 2019 | - | |
| Feb 11, 2019 | - | |
| Feb 18, 2019 | Aslan | Reconciling Termination-Insensitive NI and Declassification |
| Feb 25, 2019 | Lau | StkTokens |
| Mar 4, 2019 | Martin | Interpretation of Dependent TT in LCCCs and the Coherence Problem |
| Mar 11, 2019 | Laure Petrucci | Efficient Parameter Synthesis Using Optimised State Exploration Strategies |
| Mar 18, 2019 | Mathias | Fine- & Coarse-Grained Information Flow Control |
| Mar 25, 2019 | - | |
| Apr 1, 2019 | Simon | Practice Talk for POST: Information-Flow Control in Idris |
| Apr 8, 2019 | Magnus | Extensible Records with Scoped Labels |
| Apr 15, 2019 | Magnus | Fixpoints for the Masses: Programming with First-class Datalog Constraints |
| Apr 22, 2019 | Easter Holiday | |
| Apr 29, 2019 | Magnus | The Flix Programming Language |
| May 6, 2019 | Alix | Compiler Correctness, Verification & Secure Compilation |
| May 27, 2019 | TPBC | |
| June 3, 2019 | Jakob Von Raumer (Nottingham) | Path Spaces in Homotopy Coequalizers |
Seminars, Fall 2018
| Date | Who | Topic |
|---|---|---|
| Aug 27, 2018, 13:00-14:00 | Hans Bugge Grathwohl | Language for specifying contracts (abstract) |
| Aug 27, 2018, 14:00-15:00 | Danil Annenkov | The Call-by-Name Forcing Translation in Template Coq (abstract) |
| Sep 3, 2018, 13:00-15:00 | Morten Krogh-Jespersen | Aneris |
| Sep 10, 2018, 13:00-15:00 | Cancelled | |
| Sep 17, 2018, 13:00-15:00 | Marit Edna Ohlenbush | Aneris Examples |
| Sep 24, 2018, 13:00-15:00 | Thomas Dinsdale-Young | |
| Oct 01, 2018, 13:00-15:00 | Daniel Gratzer | Normalization by Evaluation |
| Oct 08, 2018, 13:00-15:00 | Cancelled due to EUTypes workshop | |
| Oct 15, 2018, 13:00-15:00 | ||
| Oct 22, 2018, 13:00-15:00 | Alix Trieu | Verifying constant-time implementations in a verified compilation toolchain |
| Oct 29, 2018, 13:00-15:00 | Mathias Vorreiter Pedersen | NB: Nygaard-298 |
| Nov 05, 2018, 13:00-15:00 | ||
| Nov 12, 2018, 13:00-15:00 | Jaco van de Pol | Parametric Interval Markov Chains |
| Nov 19, 2018, 13:00-15:00 | ||
| Nov 26, 2018, 13:00-15:00 | Magnus Madsen | Kaj Grønbæk visits |
| Dec 03, 2018, 13:00-15:00 | Cancelled | |
| Dec 10, 2018, 13:00-15:00 | Aslan Askarov |
Seminars in Spring 2018
We meet every Monday from 14:00 until 16:00 in Nygaard meeting room 295. This meeting is organized by Aleš Bizjak. The list of previous seminars is available here.
| Date | Who | Topic |
|---|---|---|
| Feb 05, 2018, 14:00-16:00 | Bas Spitters | Internal Universes in Models of Homotopy Type Theory (abstract) |
| Feb 12, 2018, 14:00-16:00 | Cancelled (spring break) | |
| Feb 19, 2018, 14:00-16:00 | Morten Krogh-Jespersen | TLA+ (abstract) |
| Feb 26, 2018, 14:00-16:00 | Aleš Bizjak | Iris with some support for linearity (abstract) |
| Mar 05, 2018, 14:00-16:00 | Lars Birkedal | Logical Relations for Guarded Recursive Kinds without Step-Indexing (abstract) |
| Mar 12, 2018, 14:00-16:00 | Cancelled | |
| Mar 19, 2018, 14:00-16:00 | Mathias Vorreiter Pedersen | (Towards?) encoding the ML^2 proof technique in Iris (abstract) |
| Mar 26, 2018, 14:00-16:00 | Cancelled | |
| Apr 02, 2018, 14:00-16:00 | Cancelled (Easter Monday) | |
| Apr 09, 2018, 14:00-16:00 | Dan Frumin | ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency (abstract) |
| Apr 16, 2018, 14:00-16:00 | Thomas Dinsdale-Young | Proving Termination and Liveness Properties (abstract) |
| Apr 19, 2018, 14:00-15:00 | Jan Hoffmann | Resource Analysis for Probabilistic Programs (abstract) |
| Apr 23, 2018, 14:00-16:00 | Kasper Svendsen | An Example of a Scalable Event-Driven Microservice (abstract) |
| Apr 30, 2018, 14:00-16:00 | Ian Orton | Internal Models of Cubical Type Theory (abstract) |
| May 07, 2018, 14:00-16:00 | Ranald Clouston | Things worth proving about the simply typed lambda-calculus (abstract) |
| May 14, 2018, 14:00-16:00 | Aslan Askarov | Towards a distributed programming language with dynamic information flow control (abstract) |
| May 21, 2018, 14:00-16:00 | Cancelled (Whit Monday) | |
| May 28, 2018, 14:00-16:00 | Johan Bay | COVERN: A Logic for Compositional Verification of Information Flow Control (abstract) |
| June 4, 2018, 14:00-16:00 | Cancelled | |
| June 11, 2018, 14:00-16:00 | Cancelled | |
| June 18, 2018, 14:00-16:00 | Cancelled | |
| June 20, 2018, 09:00-10:00 | Craig Mclaughlin | Triangulating Context Lemmas (abstract) |
Seminars in Fall 2017
We meet every Monday from 14:00 until 16:00 in Nygaard meeting room 295. This meeting is organized by Aleš Bizjak.
| Date | Who | Topic |
|---|---|---|
| Sep 04, 2017, 14:00-16:00 | Aleš Bizjak | Linear Iris |
| Sep 11, 2017, 14:00-16:00 | Cancelled | |
| Sep 18, 2017, 14:00-16:00 | Amin Timany | Inductive types in Coq (abstract) |
| Sep 25, 2017, 14:00-16:00 | Lars Birkedal and Mathias Høier | Distributed separation logic |
| Oct 02, 2017, 14:00-16:00 | Yue Li | Program Tailoring: Slicing by Sequential Criteria (abstract) |
| Oct 02, 2017, 15:00-16:00 | Tian Tan | Efficient and Precise Points-to Analysis: Modeling the Heap by Merging Equivalent Automata (abstract) |
| Oct 09, 2017, 14:00-16:00 | Cancelled due to PhD course on security | |
| Oct 16, 2017, 14:00-16:00 | Cancelled due to fall break | |
| Oct 23, 2017, 14:00-16:00 | Ranald Clouston | Fitch-Style Modal Lambda Calculi (abstract) |
| Oct 30, 2017, 14:00-16:00 | Andy Pitts | Nominal Cubical (part 1) (abstract) |
| Tuesday Oct 31, 2017, 14:00-16:00 | Andy Pitts | Nominal Cubical (part 2) (abstract) |
| Nov 06, 2017, 14:00-16:00 | Cancelled due to special talk | |
| Nov 13, 2017, 14:00-16:00 | Mathias Vorreiter Pedersen and Johan Bay | Analysis of resource usage (part 1) (abstract) |
| Nov 20, 2017, 14:00-16:00 | Mathias Vorreiter Pedersen and Johan Bay | Analysis of resource usage (part 2) (abstract) |
| Nov 27, 2017, 14:00-16:00 | Lars Birkedal | Mechanised Relational Verification of Concurrent Programs with Continuations (abstract) |
| Dec 04, 2017, 14:00-16:00 | Thomas Dinsdale-Young | A Perspective on Specifying and Verifying Concurrent Modules (abstract) |
| Dec 11, 2017, 14:00-16:00 | Lau Skorstengaard | A Brief Introduction to WebAssembly (abstract) |
| Dec 18, 2017, 14:00-16:00 | Cancelled |
Seminars in Spring 2017
We meet every Monday from 14:00 until 16:00 in Nygaard meeting room 395. This meeting is organized by Aleš Bizjak.
| Date | Who | Topic |
|---|---|---|
| Jan 11, 2017 15:00-16:00 | Dexter Kozen | Cantor Meets Scott: Semantic Foundations for Probabilistic Networks (abstract) |
| Jan 23, 2017 14:00 - 16:00 | Lars Birkedal | |
| Jan 30, 2017 14:00 - 16:00 | Bas Spitters | The HoTT library: a formalization of homotopy type theory in Coq (abstract) |
| Feb 06, 2017 14:00 - 16:00 | Aslan Askarov | A Calculus for Flow-Limited Authorization (abstract) |
| Feb 13, 2017 14:00 - 16:00 | Aleš Bizjak | A Split Model of Guarded Dependent Type Theory (abstract) |
| Feb 20, 2017 14:00 - 16:00 | Thomas Dinsdale-Young | Starling: Lightweight Concurrency Verification With Views (abstract) |
| Feb 27, 2017 14:00 - 16:00 | Ranald Clouston | The Many Worlds of Modal λ-calculi: I. Curry-Howard for Necessity, Possibility and Time (abstract) |
| Mar 06, 2017 14:00 - 16:00 | Daniel Huang | Semantics of probabilistic programming languages (abstract) |
| Mar 13, 2017 14:00 - 16:00 | Cancelled because of CS retreat | |
| Mar 20, 2017 14:00 - 15:00 | Kristoffer Just Andersen | Compositional Shape Analysis by means of Bi-Abduction (abstract) |
| Mar 20, 2017 15:00 - 16:00 | Felix Wiemuth | Internship report (abstract) |
| Mar 27, 2017 14:00 - 16:00 | Mathias Vorreiter Pedersen | Explicit Secrecy: A Policy for Taint Tracking (abstract) |
| Apr 03, 2017 14:00 - 16:00 | Lau Skorstengaard | Linking Types for Multi-Language Software: Have Your Cake and Eat It Too (abstract) |
| Apr 10, 2017 14:00 - 16:00 | Cancelled | |
| Apr 24, 2017 14:00 - 16:00 | Bas Spitters | Towards a proof of active security for multi-party computation in easycrypt (abstract) |
| May 01, 2017 14:00 - 16:00 | Lars Birkedal | ETAPS report, status, and planning |
| May 08, 2017 14:00 - 16:00 | Aslan Askarov | Erasure policies and disclosure vulnerabilities |
| May 15, 2017 14:00 - 16:00 | Mathias Vorreiter Pedersen | From trash to treasure: timing-sensitive garbage collection (abstract) |
| May 22, 2017 14:00 - 16:00 | Thomas Dinsdale-Young | Caper: Under the Hood (part 1) (abstract) |
| Jun 12, 2017 14:00 - 16:00 | Cancelled | |
| Jun 19, 2017 14:00 - 16:00 | Kristoffer Just Andersen | Caper: Under the Hood (part 2) (abstract) |
Seminars in Fall 2016
We meet every Monday from 14:00 until 16:00 in Nygaard meeting room 395. This meeting is organized by Aleš Bizjak.
| Date | Who | Topic |
|---|---|---|
| Aug 29, 2016 14:00 - 16:00 | Robbert Krebbers | Iris 3.0 (abstract) |
| Sep 05, 2016 14:00 - 16:00 | Kristoffer Just Andersen | Caper and permissions (abstract) |
| Sep 12, 2016 14:00 - 16:00 | Amin Timany | Simple Dependent Polymorphic I/O Effects (abstract) |
| Sep 19, 2016 14:00 - 16:00 | Mathias Vorreiter Pedersen | From trash to treasure: timing-sensitive garbage collection (abstract) |
| Sep 26, 2016 14:00 - 15:00 | Deepak Garg | Thoth: Comprehensive policy compliance in data retrieval systems (abstract) |
| Sep 26, 2016 15:00 - 16:00 | Bas Spitters and Florian Faissole | Probability theory in Coq using synthetic topology, hopefully with an application to continuous probabilistic computation (abstract) |
| Oct 03, 2016 14:00 - 16:00 | Morten Krogh-Jespersen | Verifying a queue implementation in Iris (abstract) |
| Oct 10, 2016 14:00 - 16:00 | Cancelled | |
| Oct 17, 2016 14:00 - 16:00 | Cancelled | |
| Oct 24, 2016 14:00 - 16:00 | Aleksandr Karbyshev | Compositional Noninterference for Concurrent Programs via Separation and Framing (abstract) |
| Oct 31, 2016 14:00 - 16:00 | Chuangjie Xu | A Continuous Model of Type Theory (abstract) |
| Nov 07, 2016 14:00 - 16:00 | Leo Stefanesco | A Game-Theoretic Approach to Concurrent Separation Logic (abstract) |
| Nov 14, 2016 14:00 - 16:00 | Aleš Bizjak | Cantor meets Scott: Domain-Theoretic Foundations for Probabilistic Network Programming (abstract) |
| Nov 21, 2016 14:00 - 16:00 | Radu Mardare | Towards a Quantitative Theory of Effects (abstract) |
| ** Wed ** Nov 23 13:00 - 14:00 | Gilles Barthe | ** Nygaard 295 ** TBA |
| Nov 28, 2016 14:00 - 16:00 | Mathias Høier | Diagonal Arguments and Cartesian Closed Categories (abstract) |
| Dec 05, 2016 14:00 - 15:00 | Brigitte Pientka | Programming Coinductive Proofs (abstract) |
| Dec 05, 2016 15:00 - 16:00 | Peter Dybjer | One-Dimensional Higher Inductive Types (abstract) |
| Dec 12, 2016 14:00 - 16:00 | Ranald Clouston | On Sessions and Infinite Data (abstract) |
| Dec 19, 2016 14:00 - 16:00 | Lau Skorstengaard | Tales of Belgium: Reasoning about Capability Machines using Logical Relations (abstract) |
Seminars in Spring 2016
We meet every Monday from 14:00 until 15:00 in Nygaard meeting room 395. This meeting is organized by Robbert Krebbers.
| Date | Who | Topic |
|---|---|---|
| Feb 03, 2016 13:00 - 14:30 | Egbert Rijke | Graph model of type theory (part 1) |
| Feb 05, 2016 14:30 - 16:00 | Egbert Rijke | Graph model of type theory (part 2) |
| Apr 25, 2016 14:00 - 15:00 | Dominique Devriese | Fully abstract compilation by approximate back-translation (abstract) |
| Apr 25, 2016 15:00 - 16:30 | Robbert Krebbers | Interactive separation logic proofs in Coq (abstract) |
| May 02, 2016 | Aleksandr Karbyshev | Talk about “Verified Correctness and Security of OpenSSL HMAC” (abstract) |
| May 10, 2016 | Valeria Vignudelli | Environmental Bisimulations for Probabilistic Higher-Order Languages (abstract) |
| May 23, 2016 | Aleš Bizjak | Talk about “A Lambda-Calculus Foundation for Universal Probabilistic Programming” (abstract) |
| May 30, 2016 | Gaetan Gilbert | Andromeda: handling extensional type theory (abstract) |
| Jun 02, 2016 | Ilya Sergey | Programming and Proving with Concurrent Resources (abstract) |
| Jun 06, 2016 | Lau Skorstengaard | Talk about “CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization” (abstract) |
| Jun 13, 2016 | Ranald Clouston | Talk about “Dependent Types and Fibred Computational Effects” (abstract) |
| Jun 20, 2016 | Thomas Dinsdale-Young | Caper: Automatic Verification with Concurrent Abstract Predicates (abstract) |
| Jul 14, 2016 | Ralf Jung | The Lifetime Logic – A logic for Rust-style borrowing (abstract) |
Meetings in 2014 and 2015
| Date | Who | Topic / Reading |
|---|---|---|
| Aug 18 | Kasper | RCU - Verifying Concurrent Memory Reclamation Algorithms with Grace |
| Aug 25 | Stefan/Tadeusz | TBA |
| Sep 1 | Cancelled due to ICFP | |
| Sep 8 | Aleš | Step-indexed logical relations for probability |
| Sep 15 | Ranald | Operational semantics and normalization for a programming language with guarded recursive types. |
| Sep 22 | Thomas | Game/Trace semantics (from Guilhem Jaber’s thesis) |
| Sep 29 | TBA | |
| Oct 6 | Thomas | More game semantics - Game semantics for good general references |
| Oct 13 | Fall break | |
| Oct 20 | Lars | Abstract Effects and Concurrency |
| Oct 27 | TBA | |
| Nov 3 | Pedro | TaDA |
| Nov 10 | Hans | NBE |
| Nov 17 | Aslan + Kasper | Erasure + Iris practise talk (meeting rescheduled to 15:00-17:00) |
| Nov 24 | Aslan | Hyperproperties |
| Dec 1 | Marco | PCF / FPC in Topos of Trees |
| Dec 8 | Kasper | Linearizability paper |
| Jul 6 | Ulrik Buchholtz | Weak dependent type theories |
| Jan 19 | Jesper | RTac (The meeting will be in Nygaard room 395 instead) |
| Jan 26 | Ranald | Foundational Extensible Corecursion (Blanchette et al) |
| Aleš | The coherence problem for models of DTT and some solutions | |
| Feb 2 | Kasper | Integrating Linear and Dependent Types |
| Morten | From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification. Adam Chlipala | |
| Feb 9 | Thomas | Mechanized Verification of Fine-grained Concurrent Programs |
| Aslan | TBA | |
| Feb 16 | Hans | Guarded Dependent Type Theory |
| Feb 23 | Lars | Observational Equivalence for Inductive-Coinductive Programs (The meeting will be in Nygaard room 395 instead) |
| Marco | TBA | |
| March 1 | - | Cancelled |
| March 9 | Kristoffer | Overview of Rely/Guarantee |
| Kasper | A Separation Logic for Enforcing Declarative Information Flow Control Policies | |
| March 16 | Ranald | Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus |
| Aleš | Non-wellfounded trees in Homotopy Type Theory | |
| March 23 | Morten | A logical relation for a type-and-effect system - without effects - in IRIS |
| Thomas | TBA | |
| March 30 | Aslan | TBA |
| Hans | Type-checking dependently typed languages. See the first parts of Ulf Norell’s thesis. | |
| April 6 | Cancelled due to easter | |
| April 13 | Cancelled due to ETAPS | |
| April 20 | Cancelled | |
| April 27 | Stevan Andjelkovic | Towards a Martin-Löf type theory with algebraic effects and handlers |
| Kristoffer | Overview of the Views framework | |
| May 4 | Cancelled | |
| May 11 | Lars | Dagstuhl report |
| May 18 | - | Cancelled |
| May 25 | - | Cancelled |
| June 1 | Bas | Observational Type Theory |
| Bas/Hans/Ranald | Types report | |
| June 29 | Aleksandr Karbyshev | Property-Directed Inference of Universal Invariants or Proving Their Absence |