MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

Mtac2: Strongly-Typed Tactic- and Meta-Programming for Coq

Jan-Oliver Kaiser
MMCI
SWS Student Defense Talks - Thesis Proposal
SWS  
Public Audience
English

Date, Time and Location

Wednesday, 27 May 2020
10:30
60 Minutes
E1 5
Online
Saarbr├╝cken

Abstract

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.

Contact

--email hidden

Maria-Louise Albrecht, 05/25/2020 09:12 PM -- Created document.