HTT: Hoare Type Theory

---

HTT is a verification system which incorporates Hoare style specifications via preconditions and postconditions, into types. A Hoare type {P}x : A{Q} denotes computations with a precondition P and postcondition Q, returning a value of type A. Hoare types are a dependently typed version of monads, as used in the programming language Haskell. Monads higenically combine the language features for pure functional programming, with those for imperative programming, such as state or exceptions. In this sense, HTT establishes a formal connection between Hoare logic and monads, in the style of Curry-Howard isomorphism: every effectful command in HTT has a type which corresponds to the appropriate inference rule in Hoare logic, and vice versa, every inference rule in (a version of) Hoare logic, corresponds to a command in HTT which has that rule as the type.

---

---

Source code for HTT is available here.

Supplementary material:

• Structuring the Verification of Heap-Manipulating Programs
  Aleksandar Nanevski, Viktor Vefeiadis and Josh Berfine. POPL 2010.
  
  This paper introduces what is closest to the current structure of the implementation of HTT. It puts emphasis on structuring programs and proofs together, rather than on attacking the verification problem using proof automation. It carries out a large case study, verifying the congruence closure algorithm of the Barcelogic SAT solver.
  
  The current implementation downloadable above differs from what's explained in this paper, in that it uses unary, rather than binary postconditions.


• Polymorphism and Separation in Hoare Type Theory
  Aleksandar Nanevski, Greg Morrisett and Lars Birkedal. ICFP 2006.
  
  The first paper containing a (very impoverished) definition of HTT.


• Hoare Type Theory, Polymorphism and Separation
  Aleksandar Nanevski, Greg Morrisett and Lars Birkedal. JFP 2007.
  
  Journal version of the ICFP 2006 paper.


• Abstract Predicates and Mutable ADTs in Hoare Type Theory
  Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal. ESOP 2007.
  
  Adding abstract predicates to HTT.


• A Realizability Model for Impredicative Hoare Type Theory
  Rasmus L. Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett. ESOP 2008.
  
  A semantic model for HTT, but without large sigma types.


• Ynot: Dependent Types for Imperative Programs
  Aleksandar Nanevski, Greg Morrisett, Avi Shinnar, Paul Govereau, Lars Birkedal. ICFP 2008.
  
  First implementation of HTT as a DSL in Coq, and a number of examples.


• Partiality, State and Dependent Types
  Kasper Svendsen, Lars Birkedal and Aleksandar Nanevski. TLCA 2011.
  
  A semantic model for HTT, with large sigma types.

---