Jan Smith

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. I have also been Head of the CSE department at Chalmers and University of Gothenburg.

2018-2021 I had an assignment on Artificial Intelligence from Stefan Bengtsson, the President of Chalmers. It included that I was

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

Research

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.

Address

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