Preliminary Report on the Yalla Library
Author: Olivier Laurent
Paper Information
| Title: | Preliminary Report on the Yalla Library |
| Authors: | Olivier Laurent |
| Proceedings: | Coq Abstracts |
| Editor: | Nicolas Tabareau |
| Keywords: | Coq library, linear logic, deep embedding, exchange rule, permutations, finite multisets |
| Abstract: | ABSTRACT. Yet Another deep embedding of Linear Logic in Coq We present some results and comments around the ongoing development of the Yalla library which provides a deep embedding of linear logic in Coq relying on an explicit exchange rule. |
| Pages: | 2 |
| Talk: | Jul 08 12:00 (Session 38B) |
| Paper: |  |