Axiomatic Set Theory in Type Theory

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

Gert Smolka

• Abstract, Types 2015
• Slides, Types 2015
• Draft of full paper
• Coq development, done by Dominik Kirst
  • With proofs
  • Without proofs
  • zip archive, compiles with Coq-8.4pl2