Suggested articles

Security

• A Separation Logic for Enforcing Declarative Information Flow Control Policies. David Costanzo and Zhong Shao. (Suggested presenter: Kasper)

• Dependent Information Flow Types Luísa Lourenço and Luís Caires. (Suggested presenter: Lars)

Improving Logics (speculation / lock free algo / liveness / weak memory)

• A Scalable, Correct Time-Stamped Stack. Mike Dodds, Andreas Haas and Christoph M. Kirsch. (Suggested presenter: Thomas)

• Deep Specifications and Certified Abstraction Layers. Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo.

• A Calculus for Relaxed Memory. Karl Crary and Michael Sullivan.

• The Problem of Programming Language Concurrency Semantics. Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod and Peter Sewell. (Suggested presenter: Kasper)

• From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification. Adam Chlipala. (Suggested presenter: Morton)

• Compositional Verification of Termination-Preserving Refinement of Concurrent Programs. Hongjin Liang, Xinyu Feng, and Zhong Shao. (Suggested presenter: Aleš)

Effects

Probabilistic programming

• Running Probabilistic Programs Backwards. Neil Toronto, Jay McCarthy and David Van Horn.
• Structural operational semantics for continuous state stochastic transition systems. Giorgio Bacci and Marino Miculan

Type theory / guarded recursion

• Universes and Coherence for DTT. (Suggested presenter: Aleš)

• Sized types. (Suggested presenter: Hans)

• Type checking DTT. (Suggested presenter: Hans)

• Sequent calculus in the topos of trees. Ranald Clouston and Rajeev Goré. (Suggested presenter: Ranald)

• Integrating Linear and Dependent Types. Neel Krishnaswami, Pierre Pradic and Nick Benton. (Suggested presenter: Kasper)

• Syntax and Semantics of Linear Dependent Types. Matthijs Vákár. (Suggested presenter: Aleš)

Automated analysis