The Identification of Propositions and types in Martin-Löf's Type Theory: A Programming Example. - Jan M. Smith (FCT, 1983)

Propositions and Specifications of Programs in Martin-Löfs Type Theory. - Bengt Nordström; Jan M. Smith (BIT, 1984)

An Interpretation of Martin-Lof's Type Theory in a Type-Free Theory of Propositions. - Jan M. Smith (J. Symb. Log., 1984)

Program Derivation in Type Theory: A Partitioning Problem. - Kent Petersson; Jan M. Smith (Comput. Lang., 1986)

The Strength of the Subset Type in Martin-Löf's Type Theory - Anne Salvesen; Jan M. Smith (LICS, 1988)

The Independence of Peano's Fourth Axiom from Martin-Lof's Type Theory Without Universes. - Jan M. Smith (J. Symb. Log., 1988)

Propositional Functions and Families of Types. - Jan M. Smith (Notre Dame J. Formal Log., 1989)

Type-theoretical Semantics of Some Declarative Languages. - Grigori Mints; Jan M. Smith; Enn Tyugu (Baltic Computer Science, 1991)

Kleene's Slash and Existence of Values of Open Terms in Type Theory. - Jan M. Smith (CSL, 1992)

Type Theorie Programming. - Thierry Coquand; Bengt Nordström; Jan M. Smith; Björn von Sydow (Bull. EATCS, 1994)

An Application of Constructive Completeness. - Thierry Coquand; Jan M. Smith (TYPES, 1995)

Optimized Encodings of Fragments of Type Theory in First-Order Logic. - Tanel Tammet; Jan M. Smith (J. Log. Comput., 1998)

Formal Topologies on The Set of First-Order Formulae. - Thierry Coquand; Sara Sadocco; Giovanni Sambin; Jan M. Smith (J. Symb. Log., 2000)

Inductively generated formal topologies. - Thierry Coquand; Giovanni Sambin; Jan M. Smith; Silvio Valentini (Ann. Pure Appl. Log., 2003)

Evolution and Logic. - Jan M. Smith (Epistemology versus Ontology, 2012)