The Ynot Project

The goal of the Ynot project is to make programming with dependent types practical for a modern programming language. In particular, we are extending the Coq proof assistant to make it possible to write higher-order, imperative and concurrent programs (in the style of Haskell) through a shallow embedding of Hoare Type Theory (HTT). HTT provides a clean separation between pure and effectful computations, makes it possible to formally specify and reason about effects, and is fully compositional. more...

The Ynot project is supported in part by NSF Grant 0702345, entitled Collaborative Research: Integrating Types and Verification

Who Is Involved?

Software:

The tar ball here includes a number of examples that can be type-checked with Coq.

Talks:

The Marriage of Dependent Types and Effects (Invited talk at TLCA'07)
Next Generation Type Systems (Invited talk at Microsoft Cambridge's 10th Anniversary)

Publications:

Ynot: Reasoning with the Awkward Squad
Aleksandar Nanevski, Greg Morrisett, Avi Shinnar, Paul Govereau, Lars Birkedal.
Submitted for publication. The examples from this paper can be downloaded from here, as a tar ball that includes all of the Coq sources.

Type-theoretic Semantics for Transactional Concurrency
Aleksandar Nanevski, Paul Govereau, Greg Morrisett
Submitted for publication.
Extended version available as technical report TR-09-07, Harvard University, July 2007.

A Realizability Model for Impredicative Hoare Type Theory
Rasmus L. Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett
Submitted for publication.

Hoare Type Theory, Polymorphism and Separation
Aleksandar Nanevski, Greg Morrisett, Lars Birkedal
Invited for submission to Journal of Functional Programming, January 2007.
Extended version of the ICFP'06 paper.

Abstract Predicates and Mutable ADTs in Hoare Type Theory
Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal
Proceedings of ESOP'07, pages 189-204, Braga, Portugal, March 2007.
Extended version available as technical report TR-14-06, Harvard University, September 2006.

Polymorphism and Separation in Hoare Type Theory
Aleksandar Nanevski, Greg Morrisett, Lars Birkedal
Proceedings of ICFP'06, pages 62-73, Portland, Oregon, September 2006.
Extended version available as technical report TR-10-06, Harvard University.

Dependent Type Theory of Stateful Higher-Order Functions
Aleksandar Nanevski, Greg Morrisett
Extended version available as technical report TR-24-05, Harvard University.