Carsten Führmann

Affiliate of the Marie Curie Fellowship Association. Lecturer of Computer Science at the University of Bath until February 2005. Since then, software engineer in Germany.

Email: C dot Fuhrmann at bath dot ac dot uk

Research

My research is concerned with programming languages, logics, proof theory, and category theory.

Published/accepted (in reverse chronological order)

1: Carsten Führmann and David Pym.
On categorical models of classical logic and the Geometry of Interaction.
Mathematical Structures in Computer Science, 17(5):957-1027, October 2007.
2: Carsten Führmann and David Pym.
Order-enriched categorical models of the classical sequent calculus.
J. Pure Applied Algebra, 204(1):21-78, January 2006.
3: 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.
4: Carsten Führmann and Hayo Thielecke.
On the call-by-value CPS transform and its semantics.
Information and Computation, 188(2):241-283, 2004.
5: Anna Bucalo, Carsten Führmann, and Alex Simpson.
An equational notion of lifting monad.
Theoretical Computer Science, 294:31-60, 2003.
6: 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.
7: Carsten Führmann.
The structure of call-by-value.
PhD thesis, Division of Informatics, University of Edinburgh, 2000.
8: 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.
9: 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

Teaching

Past student projects (BSc and MSc)

See here.

CM10020: Computability and decidability (Semester 2 of 2004)

(The ".pdf" files can be view with Acrobat Reader or any other PDF viewer. The ".ps.gz" files can be viewed with "ghostview", "gv", or any other Postscript viewer.)

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)

Masahito Hasegawa / David Pym / Uday Reddy / Peter Selinger / Alex Simpson / Hayo Thielecke

Validate this page