المؤلفون: Denis, Xavier, Jourdan, Jacques-Henri

المساهمون: Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Centre National de la Recherche Scientifique (CNRS), ETAPS, Sriram Sankaranarayanan, Natasha Sharygina

المصدر: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) ; https://hal.science/hal-03827702Test ; Tools and Algorithms for the Construction and Analysis of Systems (TACAS), ETAPS, Apr 2023, Paris, France. pp.93-110, ⟨10.1007/978-3-031-30820-8_9⟩ ; https://www.etaps.org/2023Test/

مصطلحات موضوعية: Rust, Deductive verification, Iterators, Closures, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], [INFO]Computer Science [cs], [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]

جغرافية الموضوع: Paris, France

العلاقة: hal-03827702; https://hal.science/hal-03827702Test; https://hal.science/hal-03827702v2/documentTest; https://hal.science/hal-03827702v2/file/main.pdfTest

الإتاحة: https://doi.org/10.1007/978-3-031-30820-8_9Test
https://hal.science/hal-03827702Test
https://hal.science/hal-03827702v2/documentTest
https://hal.science/hal-03827702v2/file/main.pdfTest

المؤلفون: Matsushita, Yusuke, Denis, Xavier, Jourdan, Jacques-Henri, Dreyer, Derek

المساهمون: Tokyo University of Science Tokyo, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Max Planck Institute for Software Systems (MPI-SWS), European Project: 683289,H2020,ERC-2015-CoG,RustBelt(2016)

المصدر: PLDI 2022 - 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation ; https://inria.hal.science/hal-03777103Test ; PLDI 2022 - 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2022, San Diego CA USA, United States. pp.841-856, ⟨10.1145/3519939.3523704⟩

مصطلحات موضوعية: CCS Concepts: • Theory of computation → Programming logic, Separation logic, Type theory Rust, verification, type systems, prophecy variables, Iris, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]

جغرافية الموضوع: San Diego CA USA, United States

العلاقة: info:eu-repo/grantAgreement//683289/EU/Logical Foundations for the Future of Safe Systems Programming/RustBelt; hal-03777103; https://inria.hal.science/hal-03777103Test; https://inria.hal.science/hal-03777103/documentTest; https://inria.hal.science/hal-03777103/file/3519939.3523704.pdfTest

الإتاحة: https://doi.org/10.1145/3519939.3523704Test
https://inria.hal.science/hal-03777103Test
https://inria.hal.science/hal-03777103/documentTest
https://inria.hal.science/hal-03777103/file/3519939.3523704.pdfTest

المؤلفون: Denis, Xavier, Jourdan, Jacques-Henri, Marché, Claude

المساهمون: Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

المصدر: ICFEM 2022 - 23th International Conference on Formal Engineering Methods ; https://hal.inria.fr/hal-03737878Test ; ICFEM 2022 - 23th International Conference on Formal Engineering Methods, Oct 2022, Madrid, Spain

مصطلحات موضوعية: Rust programming language, Deductive program verification, Aliasing and Ownership, Prophecies, Traits, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]

جغرافية الموضوع: Spain

الوقت: Madrid, Spain

العلاقة: hal-03737878; https://hal.inria.fr/hal-03737878Test; https://hal.inria.fr/hal-03737878/documentTest; https://hal.inria.fr/hal-03737878/file/main.pdfTest

الإتاحة: https://hal.inria.fr/hal-03737878Test
https://hal.inria.fr/hal-03737878/documentTest
https://hal.inria.fr/hal-03737878/file/main.pdfTest

المؤلفون: Mével, Glen, Jourdan, Jacques-Henri

المساهمون: Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Langages de programmation : systèmes de types, concurrence, preuve de programme (CAMBIUM), Collège de France (CdF (institution))-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)

المصدر: ICFP 2021 - 26th ACM SIGPLAN International Conference on Functional Programming ; https://hal.science/hal-03298759Test ; ICFP 2021 - 26th ACM SIGPLAN International Conference on Functional Programming, Aug 2021, Virtual, Japan. ⟨10.1145/3473571⟩

مصطلحات موضوعية: Separation logic, Program verification, Program specifications, Concurrency, Weak memory, Concurrent queue, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]

جغرافية الموضوع: Virtual, Japan

العلاقة: hal-03298759; https://hal.science/hal-03298759Test; https://hal.science/hal-03298759/documentTest; https://hal.science/hal-03298759/file/main.pdfTest

الإتاحة: https://doi.org/10.1145/3473571Test
https://hal.science/hal-03298759Test
https://hal.science/hal-03298759/documentTest
https://hal.science/hal-03298759/file/main.pdfTest

المؤلفون: Dang, Hoang-Hai, Jourdan, Jacques-Henri, Kaiser, Jan-Oliver, Dreyer, Derek

المساهمون: Max Planck Institute for Software Systems (MPI-SWS), Vérification d'Algorithmes, Langages et Systèmes (LRI) (VALS - LRI), Laboratoire de Recherche en Informatique (LRI), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), Université Paris-Saclay

المصدر: POPL ; https://hal.science/hal-02351793Test ; POPL, Jan 2020, New Orleans, United States. ⟨10.1145/3371101⟩ ; https://popl20.sigplan.orgTest/

مصطلحات موضوعية: Separation logic, Programming logic, Operational semantics, Rust, semantic soundness, relaxed memory models, Iris, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF]

جغرافية الموضوع: New Orleans, United States

العلاقة: hal-02351793; https://hal.science/hal-02351793Test; https://hal.science/hal-02351793/documentTest; https://hal.science/hal-02351793/file/paper.pdfTest

الإتاحة: https://doi.org/10.1145/3371101Test
https://hal.science/hal-02351793Test
https://hal.science/hal-02351793/documentTest
https://hal.science/hal-02351793/file/paper.pdfTest

المؤلفون: Jung, Ralf, Jourdan, Jacques-Henri, Krebbers, Robbert, Dreyer, Derek

المساهمون: Max Planck Institute for Software Systems (MPI-SWS), Centre National de la Recherche Scientifique (CNRS), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Université Paris-Saclay, Delft University of Technology (TU Delft)

المصدر: ISSN: 0001-0782.

مصطلحات موضوعية: Rust, safety, control, programming language, type systems, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]

العلاقة: hal-03021536; https://hal.science/hal-03021536Test; https://hal.science/hal-03021536/documentTest; https://hal.science/hal-03021536/file/jung2020safe.pdfTest

الإتاحة: https://doi.org/10.1145/3418295Test
https://hal.science/hal-03021536Test
https://hal.science/hal-03021536/documentTest
https://hal.science/hal-03021536/file/jung2020safe.pdfTest

المؤلفون: Mével, Glen, Jourdan, Jacques-Henri, Pottier, François

المساهمون: Langages de programmation, types, compilation et preuves (GALLIUM), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Vérification d'Algorithmes, Langages et Systèmes (LRI) (VALS - LRI), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Langages de programmation : systèmes de types, concurrence, preuve de programme (CAMBIUM), Collège de France (CdF (institution))-Inria de Paris, Centre National de la Recherche Scientifique (CNRS), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)

المصدر: European Symposium on Programming ; https://hal.science/hal-02183311Test ; European Symposium on Programming, Apr 2019, Prague, Czech Republic. pp.3-29, ⟨10.1007/978-3-030-17184-1_1⟩

مصطلحات موضوعية: [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]

جغرافية الموضوع: Prague, Czech Republic

العلاقة: hal-02183311; https://hal.science/hal-02183311Test; https://hal.science/hal-02183311/documentTest; https://hal.science/hal-02183311/file/main.pdfTest

الإتاحة: https://doi.org/10.1007/978-3-030-17184-1_1Test
https://hal.science/hal-02183311Test
https://hal.science/hal-02183311/documentTest
https://hal.science/hal-02183311/file/main.pdfTest

المؤلفون: de Vilhena, Paulo, Emílio, Pottier, François, Jourdan, Jacques-Henri

المساهمون: Langages de programmation : systèmes de types, concurrence, preuve de programme (CAMBIUM), Collège de France (CdF (institution))-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Université Paris-Saclay, ANR-15-CE25-0008,VOCAL,Bibliothèque OCaml vérifiée(2015)

المصدر: ISSN: 2475-1421 ; Proceedings of the ACM on Programming Languages ; https://hal.science/hal-02351562Test ; Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), ⟨10.1145/3371101⟩ ; https://popl20.sigplan.orgTest/.

مصطلحات موضوعية: Program verification, Separation logic, Least fixed point, Prophecy variables, [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF]

العلاقة: hal-02351562; https://hal.science/hal-02351562Test; https://hal.science/hal-02351562/documentTest; https://hal.science/hal-02351562/file/main.pdfTest

الإتاحة: https://doi.org/10.1145/3371101Test
https://hal.science/hal-02351562Test
https://hal.science/hal-02351562/documentTest
https://hal.science/hal-02351562/file/main.pdfTest

المؤلفون: Mével, Glen, Jourdan, Jacques-Henri, Pottier, François

المساهمون: Université Paris-Saclay, Vérification d'Algorithmes, Langages et Systèmes (LRI) (VALS - LRI), Laboratoire de Recherche en Informatique (LRI), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), Langages de programmation : systèmes de types, concurrence, preuve de programme (CAMBIUM), Collège de France (CdF (institution))-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre National de la Recherche Scientifique (CNRS), ACM

المصدر: ISSN: 2475-1421 ; Proceedings of the ACM on Programming Languages ; ICFP 2020 - 25th ACM SIGPLAN International Conference on Functional Programming ; https://hal.science/hal-02929998Test ; Proceedings of the ACM on Programming Languages, 2020, 4 (ICFP), ⟨10.1145/3408978⟩ ; https://icfp20.sigplan.orgTest/.

مصطلحات موضوعية: Separation logic, Program verification, Concurrency, Weak memory, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]

جغرافية الموضوع: New-York / Virtual, United States

العلاقة: hal-02929998; https://hal.science/hal-02929998Test; https://hal.science/hal-02929998/documentTest; https://hal.science/hal-02929998/file/mevel2020cosmo.pdfTest

الإتاحة: https://doi.org/10.1145/3408978Test
https://hal.science/hal-02929998Test
https://hal.science/hal-02929998/documentTest
https://hal.science/hal-02929998/file/mevel2020cosmo.pdfTest

المؤلفون: Denis, Xavier, Jourdan, Jacques-Henri, Marché, Claude

المساهمون: Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Inria Saclay - Île de France

المصدر: https://inria.hal.science/hal-03526634Test ; [Research Report] RR-9448, Inria Saclay - Île de France. 2021.

مصطلحات موضوعية: Rust programming language, Formal Specification, Deductive verification, Aliasing and Ownership, Prophecies, Traits, Langage de programmation Rust, Spécification formelle, Vérification Déductive, Alias, Ownership, Prophéties, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]

العلاقة: Report N°: RR-9448; hal-03526634; https://inria.hal.science/hal-03526634Test; https://inria.hal.science/hal-03526634v2/documentTest; https://inria.hal.science/hal-03526634v2/file/report.pdfTest

الإتاحة: https://inria.hal.science/hal-03526634Test
https://inria.hal.science/hal-03526634v2/documentTest
https://inria.hal.science/hal-03526634v2/file/report.pdfTest