## Author: Giselle Reis

## Paper Information

Title: | Towards a Playground for Logicians |

Authors: | Giselle Reis |

Proceedings: | WiL Short Papers and Abstracts |

Editors: | Valeria de Paiva, Amy Felty and Ursula Martin |

Keywords: | Proof theory, Mechanized proofs, Meta-theory |

Abstract: | ABSTRACT. Proving properties about proof systems is a necessary task to make sure that they are sound and satisfy basic criteria for the application being considered. Nevertheless, it is a tedious and error-prone task. In this talk, I will present on-going work on the development of a trustworthy system that helps with the verification of proof calculi's properties. This system allows for a natural specification of sequent-style calculi and visualization of rules in LaTeX. The user is also able to construct simple proof trees. Moreover, it can be used to check identity expansion, cut-elimination and permutation lemmas with the click of a button. Our goal is to free researchers from having to write down big and repetitive proofs, and move towards the use of mechanized proofs when meta-theory of proof systems is concerned. |

Pages: | 2 |

Talk: | Jul 08 15:00 (Session 40S) |

Paper: |