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

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

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

Definitions by rewriting in the Calculus of Constructions

Frédéric Blanqui
Mathematical Structures in Computer Science, 2005, 15 (1), pp.37-92. ⟨10.1017/S0960129504004426⟩
Article dans une revue inria-00105648v1
Image document

Estimation of Parallel Complexity with Rewriting Techniques

Christophe Alias , Carsten Fuhs , Laure Gonnord
Workshop on Termination, Sep 2016, Obergurgl, Austria
Communication dans un congrès hal-01345914v1
Image document

Computing Constructor Forms with Non Terminating Rewrite Programs - Extended version

Isabelle Gnaedig , Hélène Kirchner
[Research Report] 2006, pp.17
Rapport inria-00113146v1
Image document

Termination of Rewriting under Strategies

Isabelle Gnaedig , Hélène Kirchner
ACM Transactions on Computational Logic, 2009, 10 (2), pp.1-52. ⟨10.1145/1462179.1462182⟩
Article dans une revue inria-00182432v1
Image document

Higher-order dependency pairs

Frédéric Blanqui
Eighth International Workshop on Termination - WST 2006, Aug 2006, Seattle, United States
Communication dans un congrès inria-00084821v3
Image document

Complete Lattices and Up-to Techniques

Damien Pous
5th Asian Symposium on Programming Languages and Systems, Joxan Jaffar, 2007, Singapore, Singapore. pp.351-366, ⟨10.1007/978-3-540-76637-7_24⟩
Communication dans un congrès ensl-00155308v2

Divergence and unique solution of equations

Adrien Durier , Daniel Hirschkoff , Davide Sangiorgi
Logical Methods in Computer Science, 2019, ⟨10.23638/LMCS-15(3:12)2019⟩
Article dans une revue hal-02376814v1
Image document

fkcc: the Farkas Calculator

Christophe Alias
[Research Report] RR-9313, Inria. 2019
Rapport hal-02414224v1
Image document

Coverability and Termination in Recursive Petri Nets

Alain Finkel , Serge Haddad , Igor Khmelnitsky
Petri Nets 2019 / ACSD 2019 - 40th International Conference on Application and Theory of Petri Nets and Concurrency, Jun 2019, Aachen, Germany
Communication dans un congrès hal-02081019v1