The type of tactics in all (procedural) proof assistants is (a variant of) the one introduced in LCF. We discuss why this is inconvenient and we propose a new type for tactics that 1) allows the imple- mentation of more clever tactics; 2) improves the implementation of declarative languages on top of procedural ones; 3) allows for better proof structuring; 4) improves proof automation; 5) allows tactics to rearrange and delay the goals to be proved (e.g. in case of side conditions or PVS subtyping judgements).

A new type for tactics

ASPERTI, ANDREA;RICCIOTTI, WILMER;TASSI, ENRICO;SACERDOTI COEN, CLAUDIO
2009

Abstract

The type of tactics in all (procedural) proof assistants is (a variant of) the one introduced in LCF. We discuss why this is inconvenient and we propose a new type for tactics that 1) allows the imple- mentation of more clever tactics; 2) improves the implementation of declarative languages on top of procedural ones; 3) allows for better proof structuring; 4) improves proof automation; 5) allows tactics to rearrange and delay the goals to be proved (e.g. in case of side conditions or PVS subtyping judgements).
2009
PLMMS’09 Proceedings of the ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems
22
29
A. Asperti; W. Ricciotti; E. Tassi; C. Sacerdoti Coen
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/101036
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact