Zobrazeno 1 - 6
of 6
pro vyhledávání: '"Jan-Oliver Kaiser"'
Coq supports a range of built-in tactics, which are engineered primarily to support \emph{backward reasoning}. Starting from a desired goal, the Coq programmer can use these tactics to manipulate the proof state interactively, applying axioms or lemm
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1475cdec8c6885c6aef3b30aa53f9a1f
Autor:
Joseph Tassarotti, Amin Timany, Jacques-Henri Jourdan, Ralf Jung, Derek Dreyer, Robbert Krebbers, Arthur Charguéraud, Jan-Oliver Kaiser
Publikováno v:
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, 2(ICFP)
International Conference on Functional Programming (ICFP 2018)
International Conference on Functional Programming (ICFP 2018), ACM, Sep 2018, St Louis, MO, United States. pp.77, ⟨10.1145/3236772⟩
Krebbers, R, Jourdan, J-H, Jung, R, Tassarotti, J, Kaiser, J-O, Timany, A, Charguéraud, A & Dreyer, D 2018, ' MoSeL: a general, extensible modal framework for interactive proofs in separation logic ', PACMPL, bind 2, nr. ICFP, s. 77:1-77:30 . https://doi.org/10.1145/3236772
Proceedings of the ACM on Programming Languages, 2(ICFP)
International Conference on Functional Programming (ICFP 2018)
International Conference on Functional Programming (ICFP 2018), ACM, Sep 2018, St Louis, MO, United States. pp.77, ⟨10.1145/3236772⟩
Krebbers, R, Jourdan, J-H, Jung, R, Tassarotti, J, Kaiser, J-O, Timany, A, Charguéraud, A & Dreyer, D 2018, ' MoSeL: a general, extensible modal framework for interactive proofs in separation logic ', PACMPL, bind 2, nr. ICFP, s. 77:1-77:30 . https://doi.org/10.1145/3236772
A number of tools have been developed for carrying out separation-logic proofs mechanically using an interactive proof assistant. One of the most advanced such tools is the Iris Proof Mode (IPM) for Coq, which offers a rich set of tactics for making
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8b8304b64369c2034fce0d766bbd12d0
https://lirias.kuleuven.be/handle/123456789/627447
https://lirias.kuleuven.be/handle/123456789/627447
Publikováno v:
Proceedings of the ACM on Programming Languages, 2(ICFP)
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (ICFP), pp.1-31. ⟨10.1145/3236773⟩
Proceedings of the ACM on Programming Languages, 2018, 2 (ICFP), pp.1-31. ⟨10.1145/3236773⟩
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (ICFP), pp.1-31. ⟨10.1145/3236773⟩
Proceedings of the ACM on Programming Languages, 2018, 2 (ICFP), pp.1-31. ⟨10.1145/3236773⟩
Coq supports a range of built-in tactics, which are engineered primarily to support backward reasoning . Starting from a desired goal, the Coq programmer can use these tactics to manipulate the proof state interactively, applying axioms or lemmas to
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f04fcf8e3d307d4d94952473d2a99a8d
http://resolver.tudelft.nl/uuid:76e4c827-24ae-45c5-a57f-f902a6011fd8
http://resolver.tudelft.nl/uuid:76e4c827-24ae-45c5-a57f-f902a6011fd8
Autor:
Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis, Craig McLaughlin, Jan-Oliver Kaiser
Publikováno v:
ICFP
Compiler verification is essential for the construction of fully verified software, but most prior work (such as CompCert) has focused on verifying whole-program compilers. To support separate compilation and to enable linking of results from differe
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::16e82615b84db5542040088e27dda763
https://doi.org/10.1145/2858949.2784764
https://doi.org/10.1145/2858949.2784764
Publikováno v:
Certified Programs and Proofs ISBN: 9783319035444
CPP
CPP
We present a formal constructive theory of regular languages consisting of about 1400 lines of Coq/Ssreflect. As representations we consider regular expressions, deterministic and nondeterministic automata, and Myhill and Nerode partitions. We constr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e114031fa664865a7bed9579ef7de231
https://doi.org/10.1007/978-3-319-03545-1_6
https://doi.org/10.1007/978-3-319-03545-1_6
Publikováno v:
POPL
POPL, Jan 2020, New Orleans, United States. ⟨10.1145/3371101⟩
Proceedings of the ACM on Programming Languages
POPL, Jan 2020, New Orleans, United States. ⟨10.1145/3371101⟩
Proceedings of the ACM on Programming Languages
The Rust programming language supports safe systems programming by means of a strong ownership-tracking type system. In their prior work on RustBelt, Jung et al. began the task of setting Rust’s safety claims on a more rigorous formal foundation. S
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6d25cd7d72c1a39c612ac31de2108365