Extending SMT-LIB v2 with Lambda-Terms and Polymorphism
Authors: Richard Bonichon, David Déharbe and Cláudia Tavares
Paper Information
| Title: | Extending SMT-LIB v2 with Lambda-Terms and Polymorphism |
| Authors: | Richard Bonichon, David Déharbe and Cláudia Tavares |
| Proceedings: | SMT 2014 Proceedings |
| Editors: | Philipp Ruemmer and Christoph M. Wintersteiger |
| Keywords: | polymorphism, lambda expressions, typing, monomorphization, SMT-LIB, veriT |
| Abstract: | ABSTRACT. This paper describes two syntactic extensions to SMT-LIB proof scripts: lambda-expressions and polymorphism. After extending the syntax to allow these expressions, we show how to update the typing rules of the SMT-LIB to check the validity of these new terms and commands. Since most SMT-solvers only deal with many-sorted first-order formulas, we detail a monomorphization mechanism to allow to use polymorphism in SMT-LIB syntax while retaining a monomorphic solver core. |
| Pages: | 11 |
| Talk: | Jul 17 15:30 |
| Paper: |  |