Skip to Main content Skip to Navigation
Conference papers

Proof construction in linear logic and programming

Didier Galmiche 1
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this talk, we consider the problem to have efficient methods to construct proofs and proof nets in different fragments of Linear Logic (LL). Non-classical logics as intuitionistic and linear logics are used in various branches of computer science, through various programming paradigms like proof-search as computation, proofs-as-programs, proofs-as-computation, and then automated proof search (construction) methods are necessary. We will present at first methods, based for instance on canonical proofs or matrix characterizations, for proof construction in some LL fragments and their applications. Then, we will consider the notion of proof net that provides a nice, graphical representation of proofs (without some syntactical bureaucracy) and present new methods for automated proof nets construction in various fragments of LL. Relationship and comparisons between the both approaches will be discussed.
Document type :
Conference papers
Complete list of metadata
Contributor : Publications Loria <>
Submitted on : Monday, September 25, 2006 - 5:03:53 PM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM


  • HAL Id : inria-00098600, version 1



Didier Galmiche. Proof construction in linear logic and programming. COST 15 LIEGE Seminar on Non Classical Logics for Computer Science Applications, invited lecture, 1998, Liege/Belgium, 1 p. ⟨inria-00098600⟩



Record views