Mechanizing Focused Linear Logic in Coq
Electr. Notes Theor. Comput. Sci., Volume 338, 2018, Pages 219-236.
Abstract Linear logic has been used as a foundation (and inspiration) for the development of programming languages, logical frameworks and models for concurrency. Linear logicu0027s cut-elimination and the completeness of focusing are two of its fundamental properties that have been exploited in such applications. Cut-elimination guaran...More
Full Text (Upload PDF)
PPT (Upload PPT)