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

Filtrer vos résultats

103 résultats
keyword_s : Termination
Page :
triés par
Image document

Refinement Types as Higher Order Dependency Pairs

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

On Computational Interpretations of the Modal Logic S4 IIIb. Confluence, Termination of the $\lambda\mbox{ev}Q_H$-Calculus

 Jean Goubault-Larrecq
[Research Report] RR-3164, INRIA. 1997
Rapport inria-00073524v1

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
Image document

Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting

 Frédéric Blanqui , Guillaume Genestier , Olivier Hermant
FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany. ⟨10.4230/LIPIcs.FSCD.2019.9⟩
Communication dans un congrès hal-01943941v4
Image document

Static analysis by abstract interpretation of functional temporal properties of programs

 Caterina Urban
Other [cs.OH]. Ecole normale supérieure - ENS PARIS, 2015. English. ⟨NNT : 2015ENSU0017⟩
Thèse tel-01176641v2
Image document

The Heart of Intersection Type Assignment

 Steffen van Bakel
[Research Report] RR-5984, INRIA. 2006, pp.34
Rapport inria-00096419v2
Image document

Inference of ranking functions for proving temporal properties by abstract interpretation

 Caterina Urban , Antoine Miné
Computer Languages, Systems and Structures, 2015, ⟨10.1016/j.cl.2015.10.001⟩
Article dans une revue hal-01312239v1
Image document

On strong normalisation of explicit substitution calculi

 Frédéric Lang , Pierre Lescanne
[Research Report] LIP RR-1999-37, Laboratoire de l'informatique du parallélisme. 1999, 2+11p
Rapport hal-02101760v1
Image document

HORPO with Computability Closure : A Reconstruction

 Frédéric Blanqui , Jean-Pierre Jouannaud , Albert Rubio
14th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Oct 2007, Yerevan, Armenia
Communication dans un congrès inria-00168304v1
Image document

Induction for Positive Almost Sure Termination - Extended version

 Isabelle Gnaedig
[Research Report] 2007, pp.16
Rapport inria-00147450v2
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

A3PAT, an Approach for Certified Automated Termination Proofs

 Evelyne Contejean , Pierre Courtieu , Julien Forest , Andrei Paskevich , Olivier Pons , et al.
2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, ACM, Jan 2010, Madrid, Spain. pp.63-72, ⟨10.1145/1706356.1706370⟩
Communication dans un congrès inria-00535655v1
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

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
Image document

Modular termination of C programs

 Guillaume Andrieu , Christophe Alias , Laure Gonnord
[Research Report] RR-8166, INRIA. 2012
Rapport hal-00760917v2
Image document

Induction for termination with local strategies - Extended version

 Olivier Fissore , Isabelle Gnaedig , Hélène Kirchner
[Intern report] A01-R-177 || fissore01b, 2001, 29 p
Rapport inria-00107541v1
Image document

CoLoR: a Coq library on rewriting and termination

 Frédéric Blanqui , Solange Coupet-Grimal , William Delobel , Sébastien Hinderer , Adam Koprowski
Eighth International Workshop on Termination - WST 2006, Aug 2006, Seattle, United States
Communication dans un congrès inria-00084835v2
Image document

Decidable Approximations of Sets of Descendants and Sets of Normal Forms - extended version

 Thomas Genet
[Research Report] RR-3325, INRIA. 1997, pp.28
Rapport inria-00073364v1
Image document

Toward a General Rewriting-Based Framework for Reducibility

 Colin Riba
2008
Rapport hal-00779623v1
Image document

Terminaison en temps moyen fini de systèmes de règles probabilistes

 Florent Garnier
Modélisation et simulation. Institut National Polytechnique de Lorraine - INPL, 2007. Français. ⟨NNT : 2007INPL055N⟩
Thèse tel-01752898v2
Image document

Decidable Approximations of Sets of Descendants and Sets of Normal forms

 Thomas Genet
9th Conference on Rewriting Techniques and Applications, 1998, Tsukuba, Japan, pp.151-165
Communication dans un congrès inria-00098700v1
Image document

Compatibility between DAXML Schemas

 Benoît Masson , Loïc Hélouët , Albert Benveniste
[Research Report] RR-7559, INRIA. 2011, pp.36
Rapport inria-00573774v1
Image document

Curry and Howard Meet Borel

 Melissa Antonelli , Ugo Dal Lago , Paolo Pistone
LICS 2022 - 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Aug 2022, Haifa, Israel. ⟨10.1145/3531130.3533361⟩
Communication dans un congrès hal-03921650v1
Image document

Termination of rewrite relations on λ-terms based on Girard's notion of reducibility

 Frédéric Blanqui
Theoretical Computer Science, 2015, 611 (50-86), pp.37. ⟨10.1016/j.tcs.2015.07.045⟩
Article dans une revue hal-01191693v1
Image document

Termination and Confluence of Higher-Order Rewrite Systems

 Frédéric Blanqui
Rewriting Techniques and Applications, 11th International Conference, RTA 2000, Jul 2000, Norwich, United Kingdom
Communication dans un congrès inria-00105556v1
Image document

CARIBOO: A Multi-Strategy Termination Proof Tool Based on Induction

 Olivier Fissore , Isabelle Gnaedig , Hélène Kirchner
6th International Workshop on Termination 2003 - WST'03, Albert Rubio, 2003, Valencia, Spain, pp.77-79
Communication dans un congrès inria-00099467v1
Page :