PL/SE Seminar: Mtac: A Monad for Typed Tactic Programming in Coq

Speaker: Beta Ziliani , Max Planck Institute for Software Systems

Date: Tuesday, October 01, 2013

Time: 2:00 PM to 3:30 PM Note: all times are in the Eastern Time Zone

Refreshments: 2:00 PM

Public: Yes

Location: 32-D463 (Star)

Event Type:

Room Description:

Host: Adam Chlipala, CSAIL

Contact: Adam Chlipala,

Relevant URL:

Speaker URL: None

Speaker Photo:

Reminders to:,

Reminder Subject: TALK: PL/SE Seminar: Mtac: A Monad for Typed Tactic Programming in Coq

Effective support for custom proof automation is essential for large-scale interactive proof development. However, existing languages for automation via tactics either (a) provide no way to specify the behavior of tactics within the base logic of the accompanying theorem prover, or (b) rely on advanced type-theoretic machinery that is not easily integrated into established theorem provers.

We present Mtac, a lightweight but powerful extension to Coq that supports dependently-typed tactic programming. Mtac tactics have access to all the features of ordinary Coq programming, as well as a new set of typed tactical primitives. We avoid the need to touch the trusted kernel typechecker of Coq by encapsulating uses of these new tactical primitives in a monad, and instrumenting Coq so that it executes monadic tactics during type inference.

This talk will be an extended version of the one presented at ICFP this year.

Research Areas:

Impact Areas:

This event is not part of a series.

Created by Adam Chlipala Email at Thursday, August 29, 2013 at 4:58 PM.