Skip to Main content Skip to Navigation


...
inria-00555008v1  Journal articles
Sho SuzukiKeiichirou KusakariFrédéric Blanqui. Argument filterings and usable rules in higher-order rewrite systems
IPSJ Transactions on Programming, IPSJ, 2011, 4 (2), pp.1-12
...
tel-01750475v1  Theses
Guillaume Bonfante. Constructions d'ordres, analyse de la complexité
Autre [cs.OH]. Institut National Polytechnique de Lorraine, 2000. Français. ⟨NNT : 2000INPL102N⟩
...
hal-00763495v1  Conference papers
Frédéric BlanquiKim Quyen Ly. Automated verification of termination certificates
15th National Symposium of Selected ICT Problems, Dec 2012, Hanoi, Vietnam
...
hal-01424921v5  Journal articles
Frédéric Blanqui. Size-based termination of higher-order rewriting
Journal of Functional Programming, Cambridge University Press (CUP), 2018, ⟨10.1017/S0956796818000072⟩
...
tel-01415945v1  Theses
Raphaël Cauderlier. Object-Oriented Mechanisms for Interoperability between Proof Systems
Logic in Computer Science [cs.LO]. Conservatoire National Des Arts et Métiers, Paris, 2016. English
...
hal-02101787v1  Reports
Judicael Courant. Proof reconstruction (preliminary version).
[Research Report] LIP 1996-26, Laboratoire de l'informatique du parallélisme. 1996, 2+14p
inria-00436070v1  Conference papers
Jean-Pierre JouannaudVincent van Oostrom. Diagrammatic Confluence and Completion
International Conference in Automata, Languages and Programming, Paul Spirakis, Jul 2009, Rhodes, Greece. ⟨10.1007/978-3-642-02930-1_18⟩
hal-01377667v1  Book sections
Antoine SpicherJean-Louis Giavitto. Interaction-based Programming in MGS
Andrew Adamatzky. Advances in Unconventional Computing - Volume 1: Theory, 22, Springer, pp.305-342, 2017, Series: Emergence, Complexity and Computation, 978-3-319-33923-8. ⟨10.1007/978-3-319-33924-5⟩
...
tel-00672699v1  Theses
Mathieu Boespflug. Conception d'un noyau de vérification de preuves pour le λΠ-calcul modulo
Logique en informatique [cs.LO]. Ecole Polytechnique X, 2011. Français
...
hal-02435522v1  Reports
Denis Roegel. Detecting interference through graph reduction
[Research Report] Loria & Inria Grand Est. 1997
...
tel-02161197v1  Habilitation à diriger des recherches
Yves Guiraud. Rewriting methods in higher algebra
Category Theory [math.CT]. Université Paris 7, 2019
...
hal-01319677v1  Conference papers
Mark RizunJean-Christophe BachStéphane Ducasse. Code Transformation by Direct Transformation of ASTs
International Workshop on Smalltalk Technologies, Jul 2015, Brescia, Italy. ⟨10.1145/2811237.2811297⟩
...
tel-00646395v1  Theses
Philippe Beaucamps. Analyse de Programmes Malveillants par Abstraction de Comportements
Logique en informatique [cs.LO]. Institut National Polytechnique de Lorraine - INPL, 2011. Français
...
tel-00724233v2  Habilitation à diriger des recherches
Frédéric Blanqui. Terminaison des systèmes de réécriture d'ordre supérieur basée sur la notion de clôture de calculabilité
Logique [math.LO]. Université Paris-Diderot - Paris VII, 2012
...
tel-00656766v1  Habilitation à diriger des recherches
Guillaume Bonfante. Complexité implicite des calculs : interprétation de programmes
Complexité [cs.CC]. Institut National Polytechnique de Lorraine - INPL, 2011
...
tel-01749159v2  Theses
Cláudia Tavares. A type system for embedded rewriting programming
Software Engineering [cs.SE]. Université de Lorraine, 2012. English. ⟨NNT : 2012LORR0015⟩
...
hal-01097412v2  Conference papers
Ali AssafGuillaume Burel. Translating HOL to Dedukti
Fourth Workshop on Proof eXchange for Theorem Proving, PxTP'15, Aug 2015, Berlin, Germany. pp.74-88, ⟨10.4204/EPTCS.186.8⟩
...
hal-02901011v2  Journal articles
Jesper CockxNicolas TabareauThéo Winterhalter. The Taming of the Rew: A Type Theory with Computational Assumptions
Proceedings of the ACM on Programming Languages, ACM, In press, POPL 2021
...
inria-00592271v1  Journal articles
Isabelle GnaedigHélène Kirchner. Proving Weak Properties of Rewriting
Theoretical Computer Science, Elsevier, 2011, 412, pp.4405-4438. ⟨10.1016/j.tcs.2011.04.028⟩