# * Nominal Type Theory *

## by Mark Bickford, Vincent Rahli

2014

Mark and Vincent will discuss the formalization in Coq of the key elements that make Nuprl's constructive type theory a nominal type theory. Mark will explain why this is a good basis for authentication protocols as he showed in his paper on PCL, Protocol Composition Logic.