Jan Smith

I am a professor of Computing Science at the Department of Computer Science and Engineering at Chalmers University of Technology and Göteborg University and Dean of the IT University of Göteborg.

How to reach me

• Email: smith(at)chalmers.se Phone: +46 31 772 1034
• Address:

  Chalmers University of Technology
  Department of Computer Science and Engineering
  S-412 96 Göteborg
  Sweden

Teaching

• Logik och diskret matematik.
• Reading Course in Modal and Temporal Logics.
• Matematisk logik.
• Introduction to Type Theory.
• Axiomatic Set Theory.

Research

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.