Skip to Main content Skip to Navigation
Directions of work or proceedings

Theoretical Computer Science - Special issue on Proof search in Type-theoretic Languages

Didier Galmiche 1 David Pym
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The papers selected for this Special Issue address many of these topics, with foci on problems and topics, such as: How to model cut-free arithmetic for interfaces with existing proof-engines; The design of algorithms for provability or unprovability in many implicational logics; A constructive approach, leading to proved-correct procedures, or various search problems; The efficient management of linear contexts in linear logic programming; For non-trivial applications, the adaptation of a well-known procedure to increase the automation of proof-search in the Calculus of Constructions; The use of proof-nets as an alternative tool for automated deduction in linear logic; Reasoning about specifications of computation with an intuitionistic logic that includes definitions and induction; Characterization of cases in which classical provability and intuitionistic provability coincide and their relationships with uniform provability; Proof-search in intuitionistic logic viewed as a pertubation on proof-search in classical logic via a type-theoretic, and hence semantic, calculus.
Document type :
Directions of work or proceedings
Complete list of metadata
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 8:52:04 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM


  • HAL Id : inria-00099239, version 1



Didier Galmiche, David Pym. Theoretical Computer Science - Special issue on Proof search in Type-theoretic Languages. Didier Galmiche David Pym. vol. 232, n° 1-2 (vol. 232, n° 1-2), Elsevier, 333 p, 2000, Theoretical Computer Science. ⟨inria-00099239⟩



Record views