| Date | Who | Topic / Reading | | Aug 18 | Kasper | RCU - [[http://software.imdea.org/~gotsman/papers/recycling-esop13.pdf|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 - [[http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5970205&tag=1|Game semantics for good general references]] | | Oct 13 | | Fall break | | Oct 20 | Lars | [[http://research.microsoft.com/en-us/um/people/nick/paper-traces.pdf|Abstract Effects and Concurrency]] | | Oct 27 | TBA | | | Nov 3 | Pedro | [[http://www.doc.ic.ac.uk/~pmd09/research/publications/2014/ecoop/tada-a-logic-for-time-and-data-abstraction|TaDA]] | | Nov 10 | Hans | NBE | | Nov 17 | Aslan + Kasper | Erasure + Iris practise talk (meeting rescheduled to 15:00-17:00) | | Nov 24 | Aslan | [[https://www.cs.cornell.edu/fbs/publications/Hyperproperties.pdf|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 | [[http://www21.in.tum.de/~traytel/papers/fouco/index.html|Foundational Extensible Corecursion (Blanchette et al)]] | | | Aleš | The coherence problem for models of DTT and some solutions | | Feb 2 | Kasper | [[http://www.cs.bham.ac.uk/~krishnan/dlnl-paper.pdf|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 | [[http://www.cs.ru.nl/~hbasold/publications/ObsEq.pdf|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 | [[http://flint.cs.yale.edu/shao/papers/ddifc.html|A Separation Logic for Enforcing Declarative Information Flow Control Policies]] | | March 16 | Ranald | [[http://arxiv.org/abs/1404.6037|Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus]] | | | Aleš | [[https://homotopytypetheory.github.io/m-types/|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 [[http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf|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 | [[http://cs.au.dk/~birke/papers/views.pdf | 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 |