Filtrer vos résultats
- 27
- 10
- 20
- 9
- 6
- 2
- 4
- 2
- 36
- 1
- 1
- 1
- 2
- 3
- 3
- 6
- 1
- 5
- 1
- 1
- 1
- 2
- 1
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 33
- 4
- 22
- 6
- 6
- 5
- 5
- 4
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 37
- 7
- 6
- 5
- 5
- 5
- 5
- 4
- 3
- 3
- 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
37 résultats
|
|
|
triés par
|
|
|
Co-inductive Axiomatization of a Synchronous Language11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs '98), Sep 1998, Canberra, Australia. pp.387-399, ⟨10.1007/BFb0055148⟩
Communication dans un congrès
hal-00544505v1
|
||
|
|
Formal proof of a polychronous protocol for loosely time-triggered architectures5th International Conference on Formal Engineering Methods (ICFEM 2003), Nov 2003, Singapore, Singapore. pp.359-374, ⟨10.1007/978-3-540-39893-6_21⟩
Communication dans un congrès
hal-00544516v1
|
||
|
|
Un système de modules avancé pour SIGNAL[Rapport de recherche] RR-3176, INRIA. 1997
Rapport
inria-00073513v1
|
||
|
|
On the Freeze Quantifier in Constraint LTL: Decidability and Complexity12th International Symposium on Temporal Representation and Reasoning (TIME'05), Jul 2005, Burlington, United States. pp.113-121, ⟨10.1109/TIME.2005.28⟩
Communication dans un congrès
hal-03201127v1
|
||
|
|
Prioritizing the provision of urban ecosystem services in deprived areas, a question of environmental justiceAMBIO: A Journal of Environment and Society, 2020, ⟨10.1007/s13280-020-01438-1⟩
Article dans une revue
hal-03030612v1
|
||
|
|
Formal Proof of Dynamic Memory Isolation Based on MMU10th International Symposium on Theoretical Aspects of Software Engineering, Jul 2016, Shanghai, China. pp.73-80, ⟨10.1109/TASE.2016.28⟩
Communication dans un congrès
hal-01369769v1
|
||
|
|
Formal security proofs with minimal fuss: Implicit computational complexity at workInformation and Computation, 2015, 241, pp.96-113. ⟨10.1016/j.ic.2014.10.008⟩
Article dans une revue
hal-01144726v1
|
||
Experimenting with monadic equational reasoning in CoqProceedings of the 35th Meeting of the Japan Society for Software Science and Technology (JSSST 2018), Osaka-fu, Suita-shi, August 29--31, 2018, Aug 2018, Osaka, Japan
Communication dans un congrès
hal-02394861v1
|
|||
|
|
Extending Equational Monadic Reasoning with Monad Transformers26th International Conference on Types for Proofs and Programs, TYPES 2020, Mar 2020, Turin, Italy. ⟨10.4230/LIPIcs.TYPES.2020.2⟩
Communication dans un congrès
hal-02995160v1
|
||
|
|
Formal proof of dynamic memory isolation based on MMUScience of Computer Programming, 2018, 162, pp.76-92. ⟨10.1016/j.scico.2017.06.012⟩
Article dans une revue
hal-01712347v1
|
||
Implicit Computational Complexity and Applications: Resource Control, Security, Real-Number Computation[Technical Report] 2013-13, National Institute of Informatics. 2013, pp.16
Rapport
hal-01122860v1
|
|||
|
|
Reasoning about transfinite sequencesInternational Journal of Foundations of Computer Science, 2007, 18 (1), pp.87--112. ⟨10.1142/S0129054107004589⟩
Article dans une revue
hal-03189812v1
|
||
|
|
La conception d'un noyau orientée par sa preuve d'isolation mémoireCompas 2018, Jul 2018, Toulouse, France
Communication dans un congrès
hal-01819955v1
|
||
|
|
Preuve formelle d'isolation mémoire dynamique à base de MMUVingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. pp.297-300
Communication dans un congrès
hal-01122780v1
|
||
|
|
Logical relations for monadic typesMathematical Structures in Computer Science, 2008, 18 (06), pp.1169-1217. ⟨10.1017/S0960129508007172⟩
Article dans une revue
hal-03196102v1
|
||
|
|
Formal Proof of Soundness for an RL Prover[Technical Report] RR-0471, INRIA Lille - Nord Europe; Alexandru Ioan Cuza, University of Iasi. 2015, pp.27
Rapport
hal-01244578v1
|
||
|
|
A Trustful Monad for Axiomatic Reasoning with Probability and NondeterminismJournal of Functional Programming, 2021, ⟨10.1017/S0956796821000137⟩
Article dans une revue
hal-02986304v1
|
||
|
|
A Formalization of Polytime FunctionsITP 2011, Aug 2011, Nijmegen, Netherlands
Communication dans un congrès
hal-00654217v1
|
||
|
|
Reasoning about transfinite sequences (extended abstract)ATVA 2005 - 3rd International Symposium on Automated Technology for Verification and Analysis, Doron A. Peled; Yih-Kuen Tsay, Oct 2005, Taipei, Taiwan. pp.248-262, ⟨10.1007/11562948_20⟩
Communication dans un congrès
hal-03203572v1
|
||
|
|
(Co)inductive Proof Systems for Compositional Proofs in Reachability LogicJournal of Logical and Algebraic Methods in Programming, In press, ⟨10.1016/j.jlamp.2020.100619⟩
Article dans une revue
hal-02978080v1
|
||
Verifying reachability-logic properties on rewriting-logic specifications (extended version)[Technical Report] Faculty of Computer Science, University “Alexandru Ioan Cuza” of Iasi, Str. Berthelot 16, 6600-Iasi, Romania. 2015
Rapport
hal-01712416v1
|
|||
|
|
(Co)inductive Proof Systems for Compositional Proofs in Reachability LogicWorking Formal Methods Symposium, Sep 2019, Timisoara, Romania. pp. 32-47, ⟨10.4204/EPTCS.303.3⟩
Communication dans un congrès
hal-02176456v2
|
||
|
|
Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base18th International Workshop on Automated Verification of Critical Systems (AVOCS 2018), Jul 2018, Oxford, United Kingdom. ⟨10.14279/tuj.eceasst.76.1080⟩
Communication dans un congrès
hal-01816830v2
|
||
|
|
A Hierarchy of Monadic Effects for Program Verification Using Equational ReasoningMathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Oct 2019, Porto, Portugal. pp.226-254, ⟨10.1007/978-3-030-33636-3_9⟩
Communication dans un congrès
hal-02359796v1
|
||
|
|
Towards Corecursion Without Corecursion in Coq2022
Pré-publication, Document de travail
hal-03689027v4
|
||
|
|
The Steam Boiler Controller Problem in Signal-Coq[Research Report] RR-3773, INRIA. 1999
Rapport
inria-00072888v1
|
||
|
|
Vers la formalisation en Coq des transformateurs de monades modulairesTrente-et-unièmes Journées Francophones des Langages Applicatifs (JFLA 2020), Jan 2020, Gruissan, France. pp.23-30
Communication dans un congrès
hal-02434736v2
|
||
|
|
Formalising Executable Specifications of Low-Level Systems10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2018), Jul 2018, Oxford, United Kingdom. ⟨10.1007/978-3-030-03592-1_9⟩
Communication dans un congrès
hal-01829374v2
|
||
NII Shonan school on Coq[Technical Report] 2014-9, National Institute of Informatics. 2015, pp.6
Rapport
hal-01122870v1
|
|||
|
|
On the freeze quantifier in Constraint LTL: decidability and complexityInformation and Computation, 2006, 205 (1), pp.2-24. ⟨10.1016/j.ic.2006.08.003⟩
Article dans une revue
hal-03190175v1
|
- 1
- 2