PSTT10 Accepted Papers

Hereditary Substitution for Stratified System F
An overview of focusing for least and greatest fixed points in intuitionistic logic
Redundancies in Dependently Typed Lambda Calculi  and Their Relevance to Proof Search
An abstract type for constructing tactics in Coq
Proof search when equality is a logical connective: Extended Abstract