Carsten Führmann

Research

New paper

Long, self-contained article containing

• an improved axiomatization of our classical categories (which were introduced in the paper "Order-enriched categorical models of the classical sequent calculus", which is also available from this webpage),
• a strengthened version of the GoI result in our LICS paper, and
• many new results (e.g. about the MIX rule), several of which are due to Hasegawa.

Published/accepted (in reverse chronological order)

1

Carsten Führmann and David Pym.
Order-enriched categorical models of the classical sequent calculus.
J. Pure Applied Algebra, to appear.

2

Carsten Führmann and David Pym.
On the Geometry of Interaction for Classical Logic.
In Proceedings of the Nineteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2004), pages 211-220, Turku (Finland), 2004.

3

Carsten Führmann and Hayo Thielecke.
On the call-by-value CPS transform and its semantics.
Information and Computation, 188(2):241-283, 2004.

4

Anna Bucalo, Carsten Führmann, and Alex Simpson.
An equational notion of lifting monad.
Theoretical Computer Science, 294:31-60, 2003.

5

Carsten Führmann.
Varieties of effects.
In Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002), volume 2303 of LNCS, pages 144-158, Grenoble, 2002. Springer-Verlag.

6

Carsten Führmann.
The structure of call-by-value.
PhD thesis, Division of Informatics, University of Edinburgh, 2000.

7

Anna Bucalo, Carsten Führmann, and Alex Simpson.
Equational lifting monads.
In Proceedings of the 8th annual conference on Category Theory and Computer Science (CTCS'99), Electronic Notes in Theoretical Computer Science, pages 207-260, Edinburgh, 1999. Elsevier.

8

Carsten Führmann.
Direct models of the computational lambda-calculus.
In Proceedings of the 15th Conference on Mathematical Foundations of Programming Semantics (MFPS XV), volume 20 of Electronic Notes in Theoretical Computer Science, pages 147-172, New Orleans, 1999. Elsevier.

Slides of recent talks

• On the Geometry of Interaction for Classical Logic (LICS 2004)
• On the Geometry of Interaction for Classical Logic (GoI Afternoon, Queen Mary, London, November 2004). This can be seen as an update on the LICS talk. It contains new insights about MIX, as well as a generalized version of the extended GoI construction explained in the LICS paper. Details and proofs will appear in a long paper that David Pym and I will finish very soon.

Drafts and submitted papers

• A pattern-matching calculus for *-autonomous categories

The departmental Logic Seminar

Teaching

Past student projects (BSc and MSc)

CM10020: Computability and decidability (Semester 2 of 2004)

• Handout 1 (Introduction, Sets & Enumerability) pdf / ps.gz / 4 on 1 page ps.gz
• Handout 2 (Enumerability & diagonalization) pdf / ps.gz / 4 on 1 page ps.gz
• Handout 3 (Automata) pdf / ps.gz / 3 on 1 page ps.gz
• Handout 4 (Non-deterministic finite automata) pdf / ps.gz / 4 on 1 page ps.gz
• Handout 5 (NFA's & regular languages) pdf / ps.gz / 4 on 1 page ps.gz
• Handout 6 (Regular languages continued & Formal grammars) pdf / ps.gz / 4 on 1 page ps.gz
• Handout 7 (Context-free grammars) pdf / ps.gz / 4 on 1 page ps.gz
• Handout 8 (Limits of computability & Turing Machines) pdf / ps.gz / 4 on 1 page ps.gz
• Handout 9 (Uncomputability (for Turing machines)) pdf / ps.gz / 4 on 1 page ps.gz
• Proofs that the diagonal function, the self-halting function, and the halting function are not Turing-computable: pdf / ps.gz / 4 on 1 page ps.gz
• Handout 10 (Abacus machines) pdf / ps.gz / 4 on 1 page ps.gz
• Handout 11 (Recursive functions - Part 1: primitive recursion) pdf / ps.gz / 4 on 1 page ps.gz
• Handout 12 (Recursive functions - Part 2: primitive recursion (second part) & minimization) pdf / ps.gz / 4 on 1 page ps.gz
• Handout 13 (Recursive relations - Part 1) pdf / ps.gz / 4 on 1 page ps.gz
• Handout 14 (Recursive relations - Part 2) pdf / ps.gz / 4 on 1 page ps.gz
• Handout 15 (Closing the circle) pdf / ps.gz / 4 on 1 page ps.gz
• Handout 16 (Universal Turing Machine, semi-recursive relations) pdf / ps.gz / 4 on 1 page ps.gz
• Handout 17 (Revision) pdf / ps.gz / 4 on 1 page ps.gz
• Handout 18 (Revision Part 2) pdf / ps.gz / 4 on 1 page ps.gz

CM30071: Logic and its applications (Semester 2 of 2004)

• Introduction pdf / ps.gz
• Propositional logic (revision) & semantic entailment pdf / ps.gz
• Handout 1, containing both sets of slides above ps.gz
• Handout 2, Natural deduction pdf / ps.gz
• Handout 3, Soundness & Completeness pdf / ps.gz
• Handout 4, Completeness & Predicate Logic ps.gz
• Handout 5, Natural deduction for predicate logic ps.gz
• Handout 6, Natural deduction for predicate logic ps.gz
• Handout 7, Hoare logic ps.gz
• Handout 8, Hoare logic (part 2) ps.gz / pdf
• Handout 9, Sequent calculus ps.gz / pdf
• Handout 10, Sequent calculus vs. natural deduction ps.gz / pdf
• Handout 11, Sequent calculus, proof search & logic programming ps.gz / pdf
• Handout 12, Sequent calculus, proof search & logic programming (addendum). Preview of modal logic. ps.gz / pdf
• Handout 13, Modal logic ps.gz / pdf
• Handout 14, Natural deduction for modal logic ps.gz / pdf
• Handout 15, Intuitionistic logic (part 1/2) ps.gz / pdf
• Handout 16, Intuitionistic logic (part 2/2) ps.gz / pdf
• Handout 17, Lambda-calculus & Propositions-as-Types ps.gz / pdf
• Handout 18, Revision ps.gz / pdf

People (alphabetically)