English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Interactive theorem provers are tools that assist humans in constructing formal proofs. They have been the subject of over two decades of research, and are now capable of tackling problems of real practical interest in software and hardware verification. Some of the most effective of these tools are based on expressive type theories. This tutorial is about interactive theorem proving based on type theory, with a slant toward type theories, such as Nuprl and PVS, where expressive power has been pushed at the expense of traditional properties such as decidability of typechecking. The tutorial will cover type theoretic foundations, practical issues in the design of type theories for verification, and techniques for automating reasoning in the context of interactive systems. We will also cover some of the recent work on cooperation between interactive provers and with automatic verification tools such as model checkers.

Tutorial on Interactive Theorem Proving Using Type Theory