I am a professor of
Computing Science
at *Chalmers University of Technology*

From 2006 to 2018 I was also
Dean of the IT-Faculty at * University of Gothenburg* and
Director of the * IT-university
of Gothenburg*, a joint project of Chalmers and University of Gothenburg.

At present I have an assignment on Artificial Intelligence from Stefan Bengtsson, the President of Chalmers. It includes that I am

- Coordinating AI Competence for Sweden , an initiative of the Swedish government,
- Chairman of the steering group of CHAIR , an initiative of Chalmers on AI.

I'm also interested in the philosophy of mathematics and here is a 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 book has been translated into Chinese.

- 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. Proceedings of
*Types for proofs and programs.*, Torino, June 1995. LNCS 1158. -
Optimized Encodings of Fragments of Type Theory in First Order
Logic.
Written together with Tanel Tammet. Proceedings
of
*Types for proofs and programs.*, Torino, June 1995. LNCS 1158. -
Formal Topologies on the Set of First-Order Formulae.
Written together with Thierry Coquand, Sara Sadocco and Giovanni
Sambin. Journal of Symbolic Logic Vol 65, No 3, September 2000.

- Post: Department of Computer Science and Engineering, Chalmers University of Technology and University of Gothenburg, S-412 96 Gothenburg, Sweden.
- Email: smith at chalmers dot se
- Phone + 46 31 7721034