Boogie is both the name of a programming language and a (fully-automatic) deductive verification system. Both are developed at Microsoft Research and are used as back-end in various tools such as Spec#, VCC, HAVOC, Dafny, and Chalice. During my internship with K. Rustan M. Leino in 2008-2009, I worked on the type system of Boogie 2 and implemented the type encoding used in the Boogie 2 tool.
The work is described in this paper.