Research interests of Helmut Schwichtenberg
Within Mathematical Logic my interests are in proof theory, lambda calculus
and recursion theory.
In particular I am interested in theoretical and practical studies
concerning program extraction from proofs. A tool suitable for this
task is the
Minlog system
under development at the logic group of LMU. It is an interactive
proof assistant, designed to help constructing proofs (in minimal logic)
on computable functionals and inductively defined predicates.
More generally I am interested in applications of logic in computer
science. Recent slides:
-
Proofs and computations (with K. Miyamoto),
Leeds 2012
-
Computational content of coinductive proofs (with K. Miyamoto),
Cambridge 2012
-
Simultaneous inductive/coinductive definition of continuous functions
(with K. Miyamoto),
Dagstuhl 2011
-
A pointfree theory of partial continuous functionals
(with S. Huber and B. Karadais),
Chalmers 2011
-
Proofs and programs
(with D. Ratiu),
Chalmers 2011
-
Minimal from classical proofs
(with C. Senjak),
Chalmers 2011
-
Programs extracted from proofs: efficiency aspects
(with D. Ratiu),
Tokyo 2010
-
Proofs and computations,
Brünn 2010
-
Decorating proofs
(with D. Ratiu),
JAIST Kanazawa 2009
-
Linear two-sorted arithmetic,
Kyoto 2009
-
Decorating proofs
(with L. Chiarabini and D. Ratiu),
Leeds 2009
-
Program development by proof transformation,
AIST Osaka 2009
-
Program extraction in constructive analysis,
Tsukuba 2009
-
Mathematische Logik und Grundlagen der Mathematik, TU München 2005
Last change: 2012-05-13
