People: Speakers

Stefano Berardi, Universita' di Torino

• Logical Structures | video 1 | video 2 | video 3 | video 4
• Realizabiliy and Program Extraction | video 5 | video 6

Pierre-Louis Curien, University of Paris

• Computation and Normalization as Interaction | video 1 | video 2 | video 3 | video 4
• Denotational Semantics

Amy Felty, University of Ottawa

• Proof Carrying Code | video 1 | video 2 | video 3

Herman Geuvers, Nijmegen University

• Type Systems | video 1 | video 2 | video 3 | video 4 | video 5 | video 6 | video 7 | video 8
• Formalization of Mathematics

John Harrison, Intel

• Correctness of Hardware Components | video 1

Hugo Herbelin, INRIA

• Computational Content of Classical Logic | video 1 | video 2

Dale Miller, Pennsylvania State University

• Linear Logic | video 1 | video 2
• Decidability of Type Checking | video 3 | video 4

Alexandre Miquel, Chalmers University

• Advanced Topics in Type Theory | video 1 | video 2 | video 3

Sam Owre, SRI International

• Principles and Pragmatics of Subtyping in PVS | video 1

Carsten Schürmann, Yale University

• Logical Frameworks | video 1
• Theorem Proving | video 2 | video 3
• Logical Framework in TWELF | video 4

Benjamin Werner, INRIA

• Inductive Types | video 1 | video 2 | video 3 | video 4