Filtrer vos résultats
- 56
- 1
- 32
- 11
- 8
- 2
- 1
- 1
- 1
- 1
- 3
- 3
- 1
- 56
- 10
- 31
- 28
- 4
- 1
- 1
- 3
- 3
- 2
- 2
- 1
- 1
- 2
- 3
- 3
- 3
- 2
- 4
- 6
- 3
- 4
- 2
- 2
- 3
- 1
- 1
- 51
- 6
- 20
- 20
- 18
- 18
- 14
- 8
- 6
- 6
- 5
- 3
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 57
- 6
- 4
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
57 résultats
|
|
|
triés par
|
|
|
Definitions by rewriting in the Calculus of ConstructionsMathematical Structures in Computer Science, 2005, 15 (1), pp.37-92. ⟨10.1017/S0960129504004426⟩
Article dans une revue
inria-00105648v1
|
||
|
|
Higher-order dependency pairsEighth International Workshop on Termination - WST 2006, Aug 2006, Seattle, United States
Communication dans un congrès
inria-00084821v3
|
||
|
|
Termination of λΠ modulo rewriting using the size-change principle (work in progress)16th International Workshop on Termination, Jul 2018, Oxford, United Kingdom. pp. 10-14
Communication dans un congrès
hal-01944731v1
|
||
|
|
Recommandations sur les « éditeurs de la zone grise »Inria. 2023, pp.1-3
Rapport
hal-04001505v1
|
||
|
|
The computability path ordering: the end of a quest7th EACSL Annual Conference on Computer Science Logic - CSL'08, Sep 2008, Bertinoro, Italy
Communication dans un congrès
inria-00288209v2
|
||
|
|
Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations14th Annual Conference of the EACSL, Aug 2005, Oxford, United Kingdom. pp.135--150, ⟨10.1007/11538363_11⟩
Communication dans un congrès
inria-00000200v2
|
||
|
|
Type safety of rewrite rules in dependent typesFSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. pp.14, ⟨10.4230/LIPIcs.FSCD.2020.13⟩
Communication dans un congrès
hal-02981528v1
|
||
|
|
Inductive types in the Calculus of Algebraic ConstructionsFundamenta Informaticae, 2005, 65 (1-2), pp.61-86
Article dans une revue
inria-00105655v1
|
||
|
|
Definitions by Rewriting in the Calculus of Constructions16th Annual IEEE Symposium on Logic in Computer Science, Jun 2001, Boston, United States
Communication dans un congrès
inria-00105568v1
|
||
|
|
On the confluence of lambda-calculus with conditional rewritingTheoretical Computer Science, 2010, 411 (37), pp.3301-3327. ⟨10.1016/j.tcs.2009.07.058⟩
Article dans une revue
inria-00509054v1
|
||
|
|
Automated verification of termination certificates15th National Symposium of Selected ICT Problems, Dec 2012, Hanoi, Vietnam
Communication dans un congrès
hal-00763495v1
|
||
|
|
Designing a CPU model: from a pseudo-formal document to fast code3rd Workshop on: Rapid Simulation and Performance Evaluation: Methods and Tools, Jan 2011, Heraklion, Greece
Communication dans un congrès
inria-00546228v1
|
||
|
|
First steps towards the certification of an ARM simulator using CompcertFirst International Conference on Certified Programs and Proofs, Dec 2011, Hengchun, Taiwan. ⟨10.1007/978-3-642-25379-9_25⟩
Communication dans un congrès
inria-00624833v1
|
||
|
|
Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo TheoryTYPES 2020 - 26th International Conference on Types for Proofs and Programs, Mar 2020, Turino, Italy. ⟨10.4230/LIPIcs.TYPES.2020.6⟩
Communication dans un congrès
hal-03279766v2
|
||
|
|
A type-based termination criterion for dependently-typed higher-order rewrite systems15th International Conference on Rewriting Techniques and Applications - RTA'04, 2004, Aachen, Germany
Communication dans un congrès
inria-00100254v1
|
||
|
|
Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning - LPAR 2006, Nov 2006, Phnom Penh, Cambodia. ⟨10.1007/11916277_8⟩
Communication dans un congrès
inria-00084837v2
|
||
|
|
An Isabelle formalization of protocol-independent secrecy with an application to e-commerce2002
Autre publication scientifique
inria-00105606v1
|
||
|
|
Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite SystemsIEICE Transactions on Information and Systems, 2009
Article dans une revue
inria-00397820v1
|
||
|
|
Argument filterings and usable rules in higher-order rewrite systems[Research Report] IEICE-TR-SS2010-24.Vol110.N169, 2010
Rapport
inria-00543160v1
|
||
Encoding Type Universes Without Using Matching Modulo Associativity and CommutativityFSCD 2022 - 7th International Conference on Formal Structures for Computation and Deduction, Aug 2022, Haifa, Israel. pp.14, ⟨10.4230/LIPIcs.FSCD.2022.24⟩
Communication dans un congrès
hal-03708036v1
|
|||
|
|
A point on fixpoints in posets2014
Pré-publication, Document de travail
hal-01097809v1
|
||
|
|
Inductive types in the Calculus of Algebraic ConstructionsTyped Lambda Calculi and Applications, 6th International Conference, TLCA 2003, Jun 2003, Valencia, Spain
Communication dans un congrès
inria-00105617v1
|
||
|
|
Translating proofs from an impredicative type system to a predicative one31st EACSL Annual Conference on Computer Science Logic (CSL 2023), 2023, Warsaw, Poland. ⟨10.4230/LIPIcs.CSL.2023.19⟩
Communication dans un congrès
hal-03848584v2
|
||
|
|
Termination and Confluence of Higher-Order Rewrite SystemsRewriting Techniques and Applications, 11th International Conference, RTA 2000, Jul 2000, Norwich, United Kingdom
Communication dans un congrès
inria-00105556v1
|
||
|
|
Proposition d'architecture du moteur de test de conversion[Contrat] A04-R-488 || blanqui04d, 2004, 7 p
Rapport
inria-00099931v1
|
||
|
|
(HO)RPO Revisited[Research Report] RR-5972, INRIA. 2006, pp.20
Rapport
inria-00090488v3
|
||
|
|
Building Decision Procedures in the Calculus of Inductive Constructions16th EACSL Annual Conference on Computer Science and Logic - CSL 2007, Jacques Duparc, Sep 2007, Lausanne, Switzerland. ⟨10.1007/978-3-540-74915-8_26⟩
Communication dans un congrès
inria-00160586v2
|
||
|
|
Ekstrakto A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)PxTP 2019 - Sixth Workshop on Proof eXchange for Theorem Proving (PxTP), Aug 2019, Natal, Brazil. pp.27-35, ⟨10.4204/EPTCS.301.5⟩
Communication dans un congrès
hal-02200548v1
|
||
|
|
Termination of rewrite relations on λ-terms based on Girard's notion of reducibilityTheoretical Computer Science, 2015, 611 (50-86), pp.37. ⟨10.1016/j.tcs.2015.07.045⟩
Article dans une revue
hal-01191693v1
|
||
|
|
Automated Verification of Termination Certificates[Research Report] RR-6949, INRIA. 2009, pp.24
Rapport
inria-00390902v1
|
- 1
- 2