I am a professor of
Computing Science at the Department of
Computer Science and Engineering
at *Chalmers University of Technology*
and
*University of Gothenburg*

I am also

Dean of the IT-Faculty at *
University of Gothenburg*.

Director of the * IT-university
of Gothenburg*.

**Email:**`smith(at)chalmers.se`

**Phone:**+46 31 772 1034-
**Address:**

I'm also interested in the philosophy of mathematics and here is a recent paper connecting the subject with biological evolution:

- Evolution and Logic. A chapter in
*Epistemology versus Ontology*, P. Dybjer et al. (eds.), Logic, Epistemology, and the Unity of Science 27, Springer 2012.

Some expository publications:

- Martin-Löf's Type Theory. A chapter in Handbook of Logic in Computer Science. Oxford University Press, 2000. Written together with B. Nordström and K. Petersson.
- Type theory and Programming. The EATCS bulletin, February 1994. (together with Thierry Coquand, Bengt Nordström and Björn von Sydow)
- Programming in Martin-Löf's Type Theory. (A book written together with Bengt Nordström and Kent Petersson). Oxford University Press, 1990. The book is out of print, but a free version can be picked up from www.cs.chalmers.se/Cs/Research/Logic/book/

- The Identification of Propositions and Types in Martin-Löf's
Type Theory In
*Foundations of Computation Theory*, volume 158 of Lecture Notes in Computer Science, pages 445--456. Springer-Verlag, 1983. - An interpretation of Martin-Löf's type theory in a type-free
theory of propositions.
*Journal of Symbolic Logic*, 49(3):730--753, 1984. - Propositions, Types and Specifications in Martin-Löf's Type
Theory.
*BIT*, 24(3):288--301, October 1984. Written together with Bengt Nordström. - On a Nonconstructive Type Theory and Program Derivation.
In
*The Proceedings of Conference on Logic and its Applications, Bulgaria*. Plenum Press, 1986. -
Program Derivation in Type Theory: A Partitioning Problem}.
*Computer Languages*, 11(3/4):161--172, 1986. Written together with Kent Petersson -
The Independence of Peano's Fourth Axiom from Martin-Löf's
Type Theory without Universes.
*Journal of Symbolic Logic*, 53(3), 1988. -
The Strength of the Subset Type in Martin-Löf's Type Theory.
In
*Proceedings of LICS '88*, Edinburgh, 1988. IEEE. Written together with Anne Salvesen. -
Propositional Functions and Families of Types.
*Notre Dame Journal of Formal Logic*, 30(3), 1989. -
Type-theoretical semantics of some declarative languages.
In D. Björner, editor,
*Selected Works of Baltic Republics Computer Scientists*. Lecture Notes in Computer Science, Springer Verlag, 1991. Written together with Grigory Mints and Enn Tyugu. -
An Interpretation of Kleene's Slash in Type Theory in
*Logical Environments*, G. Huet and G. Plotkin (eds.), Cambridge University Press, 1993. -
Kleene's Slash and Existence of Values of Open Terms in Type
Theory.
*Selected Papers from CSL'92*, E. Boerger et. al. (eds.), LNCS, Springer-Verlag, 1993. -
An Application of Constructive Completeness.
Written together with Thierry Coquand. To appear in the proceedings of
*Types for proofs and programs.*, Torino, June 1995. To be published in LNCS. -
Optimized Encodings of Fragments of Type Theory in First Order
Logic.
Written together with Tanel Tammet. To appear in the proceedings
of
*Types for proofs and programs.*, Torino, June 1995. To be published in LNCS. - Formal Topologies on the Set of First-Order Formulae. Written together with Thierry Coquand, Sara Sadocco and Giovanni Sambin. To appear in Journal of Symbolic Logic.