This is a reading group where we discuss research topics regarding LF and logical reasoning. Meetings take place on Mondays at 3 PM in Carsten's office.

Feb. 8: Contextual Modal Logic and Contextual Modal Type Theory [cs]
based on Aleksandar Nanevski, Frank Pfenning and Brigitte Pientka: Contextual modal type theory

## Next week

based on:

Composing contracts: an adventure in financial engineering (functional pearl), by Simon Peyton Jones, Jean-Marc Eber and Julian Seward (2000)

Certified symbolic management of financial multi-party contracts, by Patrick Bahr, Jost Berthold, Martin Elsman (2015)

## Past topics

slides

Oct. 31: A brief introduction to bigraphs [gr]Oct. 17: Behavioral Types and Logical Frameworks [cs]Oct. 10: The cX calculus, reducing modulo congruence relation [dz]slides

Oct. 3: Focusing in Linear Logic [pbb]Aug. 22: Selene in Celf: formalising voting protocols in linear logic [ab]slides

Process calculus for standard classical logic, an investigation [dz]based on Wadler's CP calculus

Jun: Zap logic [ic][description]

May: Coherence proofs and session types [cs][description]

Apr. 11 + Apr. 18: A calculus for classical logic with explicit structural rules [dz]based on "A calculus for classical logic with explicit structural rules"

Mar. 7: Polarised Focusing in (one-sided) Classical Linear Logic [pbb]Jean-Marc Andreoli. "Logic Programming with Focussing Proofs in Linear Logic"

Feb 29: Finite Variant and Equational Theories [ab]based on

Comon-Lundh, Hubert, and Stéphanie Delaune. "The finite variant property: How to get rid of some algebraic properties."

Escobar, Santiago, José Meseguer, and Ralf Sasse. "Effectively checking the finite variant property."

Feb 15:Canonical forms in LFbased on ???

Feb. 8:Contextual Modal Logic and Contextual Modal Type Theory [cs]based on Aleksandar Nanevski, Frank Pfenning and Brigitte Pientka: Contextual modal type theory

Feb. 1: Proof Search in Proverif + Stateful verification using Horn clauses[ab]based on

1. Bruno Blanchet: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules

2. Bruni, Mödersheim, Nielson, Nielson: Set-π: Set Membership π-calculus

Jan. 25:Concurrent Logical Framework [cs]based on ???

Jan. 18:Linear reasoning and focusing [cs]based on ???