Recherche - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu

Filtrer vos résultats

215 résultats
keyword_s : Rewriting

Rule based programming in Java for protocol verification

Horatiu Cirstea , Pierre-Etienne Moreau , Antoine Reilles
5th International Workshop on Rewriting Logic and its Applications - WRLA'2004, Narciso Marti-Oliet, 2004, Barcelona, Spain. 18 p, ⟨10.1016/j.entcs.2004.06.022⟩
Communication dans un congrès inria-00100025v1

Certification of Termination Proofs Using Polynomial Interpretations

Sébastien Hinderer
17th European Summer School in Logic, Language and Information - ESSLLI '05, Aug 2005, Edimbourg/Grande Bretagne
Communication dans un congrès inria-00001205v1
Image document

Représentation et interaction des preuves en superdéduction modulo

Clément Houtmann
Génie logiciel [cs.SE]. Université Henri Poincaré - Nancy I, 2010. Français. ⟨NNT : 2010NAN10026⟩
Thèse tel-00553219v1
Image document

Refinement Types as Higher Order Dependency Pairs

Cody Roux
[Research Report] 2011, pp.19
Rapport inria-00552046v2
Image document

Introduction to the Rewriting Calculus

Horatiu Cirstea , Claude Kirchner
[Research Report] RR-3818, INRIA. 1999, pp.50
Rapport inria-00072840v1
Image document

Theorem Proving Modulo

Gilles Dowek , Thérèse Hardin , Claude Kirchner
[Research Report] RR-3400, INRIA. 1998, pp.27
Rapport inria-00077199v1

Encoding the Hydra battle as a rewrite system

Hélène Touzet
International Symposium on the Mathematical Foundations of Computer Science - MFCS'98, Aug 1998, Brno, Czech Republic, pp.267-276
Communication dans un congrès inria-00098575v1

Algorithms and Reductions for Rewriting Problems

Rakesh Verma , Michaël Rusinowitch , Denis Lugiez
Proceedings 9th Conference on Rewriting Techniques and Applications, 1998, Tsukuba, Japan, pp.166-180
Communication dans un congrès inria-00098607v1

On the Exploration of the Query Rewriting Space with Existential Rules

Mélanie König , Michel Leclère , Marie-Laure Mugnier , Michaël Thomazo
[Research Report] RR-13016, Lirmm. 2013
Rapport lirmm-00825634v1
Image document

Factorize Factorization

Beniamino Accattoli , Claudia Faggian , Giulio Guerrieri
CSL 2021 - 29th EACSL Annual Conference on Computer Science Logic, Jan 2021, Ljubljana, Slovenia. ⟨10.4230/LIPIcs.CSL.2021.22⟩
Communication dans un congrès hal-03044338v1

Towards an Automatic Analysis of Web Service Security

Yannick Chevalier , Denis Lugiez , Michael Rusinowitch
6th International Symposium on Frontiers of Combining Systems - FroCoS'07, Sep 2007, Liverpool, United Kingdom. pp.133-147, ⟨10.1007/978-3-540-74621-8_9⟩
Communication dans un congrès istex inria-00557707v1
Image document

Tactics for Reasoning modulo AC in Coq

Thomas Braibant , Damien Pous
Certified Proofs and Programs, 2011, Taiwan. pp167-182, ⟨10.1007/978-3-642-25379-9_14⟩
Communication dans un congrès hal-00484871v4
Image document

Gouvernance et étude de l'impact du changement des processus métiers sur les architectures orientées services : une approche dirigée par les modèles

Karim Dahman
Architectures Matérielles [cs.AR]. Université de Lorraine, 2012. Français. ⟨NNT : 2012LORR0241⟩
Thèse tel-01749632v2
Image document

Définitions par réécriture dans le lambda-calcul : confluence, réductibilité et typage

Colin Riba
Autre [cs.OH]. Institut National Polytechnique de Lorraine, 2007. Français. ⟨NNT : 2007INPL102N⟩
Thèse tel-01752911v1
Image document

Asymptotic Determinacy of Path Queries using Union-of-Paths Views

Nadime Francis
18th International Conference on Database Theory (ICDT 2015), Mar 2015, Brussels, Belgium. ⟨10.4230/LIPIcs.ICDT.2015.44⟩
Communication dans un congrès hal-01150780v1
Image document

Proof reconstruction (preliminary version).

Judicael Courant
[Research Report] LIP 1996-26, Laboratoire de l'informatique du parallélisme. 1996, 2+14p
Rapport hal-02101787v1
Image document

Using Deduction Modulo in Set Theory

Pierre Halmagrand
SETS14, 1st International Workshop about Sets and Tools, Jun 2014, Toulouse, France. pp.12
Communication dans un congrès hal-01100512v1
Image document

Some Axioms for Mathematics

Frédéric Blanqui , Gilles Dowek , Émilie Grienenberger , Gabriel Hondet , François Thiré
FSCD 2021 - 6th International Conference on Formal Structures for Computation and Deduction, Jul 2021, Buenos Aires / Virtual, Argentina. ⟨10.4230/LIPIcs.FSCD.2021.20⟩
Communication dans un congrès hal-03279749v1
Image document

Behavior Abstraction in Malware Analysis

Philippe Beaucamps , Isabelle Gnaedig , Jean-Yves Marion
1st International Conference on Runtime Verification, Howard Barringer, Klaus Havelund, Insup Lee, Nov 2010, St. Julians, Malta. pp.168-182, ⟨10.1007/978-3-642-16612-9_14⟩
Communication dans un congrès inria-00536500v1

Projet GasEl. Elaboration d'un logiciel de génération de mécanismes détaillés d'oxydation et de combustion de molécules d'hydrocarbures. Rapport No 5

Liliana Ibanescu , Hélène Kirchner , Olivier Bournez , Guy-Marie Côme , Gérard Scacchi , et al.
[Contrat] A03-R-541 || ibanescu03b, 2003, 42 p
Rapport inria-00099760v1
Image document

Unbounded Proof-Length Speed-up in Deduction Modulo

Guillaume Burel
16th EACSL Annual Conference on Computer Science and Logic - CSL 2007, Jacques Duparc, Sep 2007, Lausanne, Switzerland. pp.496-511, ⟨10.1007/978-3-540-74915-8_37⟩
Communication dans un congrès inria-00138195v3
Image document

Higher-dimensional normalisation strategies for acyclicity

Yves Guiraud , Philippe Malbos
Advances in Mathematics, 2012, 231 (3-4), pp.2294-2351. ⟨10.1016/j.aim.2012.05.010⟩
Article dans une revue hal-00531242v3
Image document

CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates

Frédéric Blanqui , Adam Koprowski
Mathematical Structures in Computer Science, 2011, 21 (4), pp.827-859. ⟨10.1017/S0960129511000120⟩
Article dans une revue inria-00543157v1

A Computability Path Ordering for Polymorphic Terms

Jean-Pierre Jouannaud , Jian-Qi Li
11th International Workshop on Termination, Jul 2010, Edinburgh, United Kingdom
Communication dans un congrès inria-00497405v1
Image document

The Taming of the Rew: A Type Theory with Computational Assumptions

Jesper Cockx , Nicolas Tabareau , Théo Winterhalter
Proceedings of the ACM on Programming Languages, 2021, POPL 2021, ⟨10.1145/3434341⟩
Article dans une revue hal-02901011v2
Image document

Size-based termination of higher-order rewriting

Frédéric Blanqui
Journal of Functional Programming, 2018, ⟨10.1017/S0956796818000072⟩
Article dans une revue hal-01424921v5
Image document

Computability Closure: Ten Years Later

Frédéric Blanqui
Colloquium in honor of Jean-Pierre Jouannaud, Jun 2007, Cachan, France. ⟨10.1007/978-3-540-73147-4_4⟩
Communication dans un congrès inria-00161092v1

A Rho Cube

Horatiu Cirstea , Claude Kirchner , Luigi Liquori
[Intern report] A00-R-344 || cirstea00d, LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2000, 18 p
Rapport inria-00099309v1

Outermost ground termination - Extended version

Olivier Fissore , Isabelle Gnaedig , Hélène Kirchner
[Intern report] A02-R-493 || fissore02d, 2002, 38 p
Rapport inria-00101079v1
Image document

CARIBOO: An Induction Based Proof Tool for Termination with Strategies

Olivier Fissore , Isabelle Gnaedig , Hélène Kirchner
Fourth International Conference on Principles and Practice of Declarative Programming - PPDP'02, Oct 2002, Pittsburgh, USA, 12 p
Communication dans un congrès inria-00107557v1