Ident. | Authors (with country if any) | Title |
---|
000081 |
Didier Galmiche [France] ; Daniel Mery [France] | A Connection-based Characterization of Bi-intuitionistic Validity |
000122 |
Didier Galmiche [France] ; Yakoub Salhi [France] | Sequent calculi and decidability for intuitionistic hybrid logic |
000136 |
Olfa Mosbahi [Allemagne] ; Mohamed Khalgui [Allemagne] | Combining formal methods for the development of reactive systems : DEVELOPMENT OF EMBEDDED SYSTEMS: MODELLING, VERIFICATION, SCHEDULING, IMPLEMENTATION AND RECONFIGURATION |
000171 |
Joris Rehm [France] | Proved development of the real-time properties of the IEEE 1394 Root Contention Protocol with the event-B method |
000260 |
BOULBABA BEN AMMAR [France, Tunisie] ; MOHAMED TAHAR BHIRI [Tunisie] ; Jeanine Souquieres [France] | Modélisation événementielle pour la construction de diagrammes de classes |
000342 |
Olivier Chevassut [États-Unis] ; Pierre-Alain Fouque [France] ; Pierrick Gaudry [France] ; David Pointcheval [France] | The Twist-AUgmented Technique for Key Exchange |
000375 |
Nazim Benaïsa [France] ; Dominique Cansell [France] ; Dominique Méry [France] | Integration of security policy into system modeling |
000397 |
Silvio Ghilardi [Italie] ; Enrica Nicolini [Italie] ; Silvio Ranise [Italie, France] ; Daniele Zucchelli [Italie, France] | Deciding extensions of the theory of arrays by integrating decision procedures and instantiation strategies |
000398 |
Maria Paola Bonacina [Italie] ; Silvio Ghilardi [Italie] ; Enrica Nicolini [Italie] ; Silvio Ranise [Italie, France] ; Daniele Zucchelli [Italie, France] | Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures |
000473 |
Alessandro Armando [Italie] ; Maria Paola Bonacina [Italie] ; Silvio Ranise [France] ; Stephan Schulz [Italie] | On a rewriting approach to satisfiability procedures : Extension, combination of theories and an experimental appraisal |
000476 |
Francois Lamarche [France] ; Lutz Strassburger [Allemagne] | Naming proofs in classical propositional logic |
000632 |
David Deharbe [Brésil] ; Abdessamad Imine [France] ; Silvio Ranise [France] | Abstraction-driven verification of array programs |
000642 |
Damien Stehle [France] ; Paul Zimmermann [France] | A binary recursive Gcd algorithm |
000693 |
Lutz Strassburger [France] | MELL in the calculus of structures |
000700 |
Dominique Cansell [France] ; Dominique Méry [France] | Foundations of the B method |
000719 |
Jean-Raymond Abrial ; Dominique Cansell [France] | Click'n prove: Interactive proofs within Set Theory |
000732 |
Alessandro Armando [Italie] ; Silvio Ranise [Italie, France] ; Michaël Rusinowitch [France] | A rewriting approach to satisfiability procedures |
000786 |
Philippe De Groote [France] | On the strong normalisation of intuitionistic natural deduction with permutation-conversions |
000813 |
Eric Deplagne [France] ; Claude Kirchner [France] | Deduction versus computation: The case of induction |
000886 |
D. Larchey-Wendling [France] ; D. Mery [France] ; Didier Galmiche [France] | STRIP : Structural sharing for efficient proof-search |
000890 |
Didier Galmiche [France] ; Daniel Mery [France] | Proof-search and countermodel generation in propositional BI logic |
000901 |
Guy Perrier [France] | Intuitionistic multiplicative proof nets as models of directed acyclic graph descriptions |
000954 |
| Proof-search in Type-theoretic Languages |
000969 |
A. Bouhoula [États-Unis, France] ; J.-P. Jouannaud [France] ; J. Meseguer [États-Unis] | Specification and proof in membership equational logic |
000970 |
J. L. Caldwell [États-Unis] ; I. P. Gent [Royaume-Uni] ; J. Underwood [Royaume-Uni] | Search algorithms in type theory |
000975 |
Philippe De Groote [France] | Proof-search in implicative linear logic as a matching problem |
000A14 |
G. Nadathur [États-Unis] | Correspondences between classical, intuitionistic and uniform provability |
000A16 |
D. Galmiche [France] | Connection methods in linear logic and proof nets construction |
000C78 |
N. Berregeb [France] ; A. Bouhoula [France] ; M. Rusinowitch [France] | SPIKE-AC : A system for proofs by induction in associative-commutative theories |
000D01 |
C. Hintermeier [France] ; H. Kirchner [France] ; P. D. Mosses [Danemark] | Combining algebraic and set-theoretic specifications |
000D42 |
D. Galmiche [France] ; G. Perrier | On proof normalization in linear logic |