Vol. 9 No. 2 (2016)

Articles

• Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers

  José Grimm

  1 -52

  • PDF

• Formalization of the pumping lemma for context-free languages

  Marcus V M Ramos, José Carlos Bacelar Almeida, Nelma Moreira, Ruy José Guerra Barretto de Queiroz

  53-68

  • PDF

• Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC

  YuHui Lin, Gudmund Grov, Rob Arthan

  69-130

  • PDF

• Lawvere-Tierney sheafification in Homotopy Type Theory

  Kevin Quirin, Nicolas Tabareau

  131-161

  • PDF