Seminar, Fall 2019
We meet every Monday from 13:00 until 15:00 in Nygaard-395. This meeting is organized by Danil Annenkov.
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 | Call-by-Push-Value (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.
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