HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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

https://hal.inria.fr/inria-00099239
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 8:52:04 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM

Identifiers

  • HAL Id : inria-00099239, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

66