Zobrazeno 1 - 5
of 5
pro vyhledávání: '"Paulo Emílio de Vilhena"'
Publikováno v:
Logical Methods in Computer Science, Vol Volume 19, Issue 4 (2023)
We apply program verification technology to the problem of specifying and verifying automatic differentiation (AD) algorithms. We focus on define-by-run, a style of AD where the program that must be differentiated is executed and monitored by the aut
Externí odkaz:
https://doaj.org/article/c3eb8936345649fda3bf96782f94e5cb
Publikováno v:
Programming Languages and Systems ISBN: 9783031300431
We consider a simple yet expressive $$\lambda $$ λ -calculus equipped with references, effect handlers, and dynamic allocation of effect labels, and whose operational semantics does not involve coercions or rely on type information. We equip this la
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2a19cc61d7dc9f7508574ba63a9be869
https://doi.org/10.1007/978-3-031-30044-8_9
https://doi.org/10.1007/978-3-031-30044-8_9
Publikováno v:
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2021, 5 (POPL), ⟨10.1145/3434314⟩
Proceedings of the ACM on Programming Languages, 2021, 5 (POPL), ⟨10.1145/3434314⟩
Proceedings of the ACM on Programming Languages, ACM, 2021, 5 (POPL), ⟨10.1145/3434314⟩
Proceedings of the ACM on Programming Languages, 2021, 5 (POPL), ⟨10.1145/3434314⟩
International audience; User-defined effects and effect handlers are advertised and advocated as a relatively easy-to-understand and modular approach to delimited control. They offer the ability of suspending and resuming a computation and allow info
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4b92d5e5e1d45e5e009d6ff373361c3b
https://doi.org/10.1145/3434314
https://doi.org/10.1145/3434314
Publikováno v:
Automated Reasoning
IJCAR 2020-International Joint Conference on Automated Reasoning
IJCAR 2020-International Joint Conference on Automated Reasoning, Jul 2020, Paris, France. pp.204-220, ⟨10.1007/978-3-030-51054-1_12⟩
Automated Reasoning-10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Automated Reasoning
Automated Reasoning ISBN: 9783030510534
IJCAR (2)
IJCAR 2020-International Joint Conference on Automated Reasoning
IJCAR 2020-International Joint Conference on Automated Reasoning, Jul 2020, Paris, France. pp.204-220, ⟨10.1007/978-3-030-51054-1_12⟩
Automated Reasoning-10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Automated Reasoning
Automated Reasoning ISBN: 9783030510534
IJCAR (2)
International audience; A fundamental theorem states that every field admits an algebraically closed extension. Despite its central importance, this theorem has never before been formalised in a proof assistant. We fill this gap by documenting its fo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::80cbcd464c4d1168c1a47c7e946e87e4
https://inria.hal.science/hal-03083589/file/main.pdf
https://inria.hal.science/hal-03083589/file/main.pdf
Publikováno v:
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2020, 4 (POPL), ⟨10.1145/3371101⟩
Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), ⟨10.1145/3371101⟩
Proceedings of the ACM on Programming Languages, ACM, 2020, 4 (POPL), ⟨10.1145/3371101⟩
Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), ⟨10.1145/3371101⟩
International audience; We verify the partial correctness of a "local generic solver", that is, an on-demand, incremental, memoizing least fixed point computation algorithm. The verification is carried out in Iris, a modern breed of concurrent separa
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1a8f73dced264c8159da15fea52104d9
https://hal.archives-ouvertes.fr/hal-02351562/file/main.pdf
https://hal.archives-ouvertes.fr/hal-02351562/file/main.pdf