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.
Type de document :
Direction d'ouvrage, Proceedings, Dossier
Didier Galmiche David Pym. vol. 232, n° 1-2 (vol. 232, n° 1-2), Elsevier, 333 p, 2000, Theoretical Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00099239
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:52:04
Dernière modification le : jeudi 11 janvier 2018 - 06:20:14

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

94