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. Asperti, W. Ricciotti, E. Tassi, C. Sacerdoti Coen (2009). A new type for tactics. s.l : s.n.
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).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.
