Skip to main content
guest
Join

Help

Sign In
Programming, Logic and Semantics Research Group at ITU
Home
guest

Join

Help

Sign In
Programming, Logic and Semantics Research Group at ITU
Wiki Home
Recent Changes
Pages and Files
Members
Favorites
20
All Pages
20
home
Concurrency Theory Reading Group
Directions
LF Reading Group
Past news
People
Projects
Seminar on Semantics of Linear Logic
Talks
Teaching
Type theory seminar
Add
Add "All Pages"
Done
LF Reading Group
Edit
27
…
0
Tags
No tags
Notify
RSS
Backlinks
Source
Print
Export (PDF)
This is a reading group where we discuss research topics regarding LF and logical reasoning.
Past topics
Feb. 13:Formal reasoning about financial derivatives [dz]
based on:
Composing contracts: an adventure in financial engineering (functional pearl)
, by Simon Peyton Jones, JeanMarc Eber and Julian Seward (2000)
Certified symbolic management of financial multiparty contracts
, by Patrick Bahr, Jost Berthold, Martin Elsman (2015)
Nov. 28: Twelf tutorial [cs]
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]
May: Coherence proofs and session types [cs]
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 (onesided) Classical Linear Logic [pbb]
JeanMarc Andreoli.
"Logic Programming with Focussing Proofs in Linear Logic"
Feb 29: Finite Variant and Equational Theories [ab]
based on
ComonLundh, 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 LF
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]
Jan. 18:
Linear reasoning and focusing [cs]
Javascript Required
You need to enable Javascript in your browser to edit pages.
help on how to format text
Turn off "Getting Started"
Home
...
Loading...
Past topics
based on:
Composing contracts: an adventure in financial engineering (functional pearl), by Simon Peyton Jones, JeanMarc Eber and Julian Seward (2000)
Certified symbolic management of financial multiparty contracts, by Patrick Bahr, Jost Berthold, Martin Elsman (2015)
slides
slides
slides
based on Wadler's CP calculus
based on "A calculus for classical logic with explicit structural rules"
JeanMarc Andreoli. "Logic Programming with Focussing Proofs in Linear Logic"
based on
ComonLundh, 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."
based on Aleksandar Nanevski, Frank Pfenning and Brigitte Pientka: Contextual modal type theory
based on
1. Bruno Blanchet: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules
2. Bruni, Mödersheim, Nielson, Nielson: Setπ: Set Membership πcalculus