SWS   Info

Public Audience

English

60 Minutes

Saarbrücken

With growing interest in interactive theorem proving comes an increasing
demand for proof automation. In many interactive proof assistants proof
automation means constructing tactics that perform proof steps
automatically.

In systems such as Coq, following the Curry-Howard Correspondence,
proofs are terms and tactics are metaprograms. Proof scripts produce
proof terms step by step until the resulting term inhabits the type
dictated by the theorem to be proved. Consequently, metaprogramming
facilities are vital to perform large scale proof mechanizations in Coq.

While Coq offers several mechanism for metaprogram (and tactic)
construction they all come with severe restrictions on either
applicability or expressiveness. With our work on Mtac2, a
metaprogramming and tactic language for Coq, we aim to offer an
alternative that covers a large set of use cases while simultaneously
offering static type guarantees about the output of metaprograms and
tactics.

--email hidden

passcode not visible

logged in users only