Zobrazeno 1 - 10
of 51
pro vyhledávání: '"Hugo Herbelin"'
Autor:
Nuria Brede, Hugo Herbelin
Publikováno v:
LICS
LICS 2021-36th Annual Symposium on Logic in Computer Science
LICS 2021-36th Annual Symposium on Logic in Computer Science, Jun 2021, Rome / Virtual, Italy
Logic in Computer Science
Logic in Computer Science, Jun 2021, Rome, Italy
LICS 2021-36th Annual Symposium on Logic in Computer Science
LICS 2021-36th Annual Symposium on Logic in Computer Science, Jun 2021, Rome / Virtual, Italy
Logic in Computer Science
Logic in Computer Science, Jun 2021, Rome, Italy
We develop an approach to choice principles and their contrapositive bar-induction principles as extensionality schemes connecting an "intensional" or "effective" view of respectively ill-and well-foundedness properties to an "extensional" or "ideal"
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c03f3d4af67326be534ef10a23450448
https://doi.org/10.1109/lics52264.2021.9470523
https://doi.org/10.1109/lics52264.2021.9470523
Autor:
Étienne Miquey, Hugo Herbelin
Publikováno v:
LICS
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '20), July 8--11, 2020, Saarbrücken, Germany
LICS 2020-35th ACM/IEEE Symposium on Logic in Computer Science
LICS 2020-35th ACM/IEEE Symposium on Logic in Computer Science, Jul 2020, Saarbrücken / Virtual, Germany. pp.564-577, ⟨10.1145/3373718.3394792⟩
LICS 2020-Thirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science
LICS 2020-Thirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2020, Saarbrücken, Germany
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '20), July 8--11, 2020, Saarbrücken, Germany
LICS 2020-35th ACM/IEEE Symposium on Logic in Computer Science
LICS 2020-35th ACM/IEEE Symposium on Logic in Computer Science, Jul 2020, Saarbrücken / Virtual, Germany. pp.564-577, ⟨10.1145/3373718.3394792⟩
LICS 2020-Thirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science
LICS 2020-Thirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2020, Saarbrücken, Germany
LICS 2020 will be held online; International audience; The call-by-need evaluation strategy for the λ-calculus is an evaluation strategy that lazily evaluates arguments only if needed, and if so, shares computations across all places where it is nee
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9375a571b5c9ddc3631a0671bbdffc05
https://doi.org/10.1145/3373718.3394792
https://doi.org/10.1145/3373718.3394792
Autor:
Étienne Miquey, Hugo Herbelin
Publikováno v:
FOSSACS 18-21st International Conference on Foundations of Software Science and Computation Structures
FOSSACS 18-21st International Conference on Foundations of Software Science and Computation Structures, Apr 2018, Thessalonique, Greece. pp.276-292, ⟨10.1007/978-3-319-89366-2_15⟩
Lecture Notes in Computer Science ISBN: 9783319893655
FoSSaCS
FOSSACS 18-21st International Conference on Foundations of Software Science and Computation Structures, Apr 2018, Thessalonique, Greece. pp.276-292, ⟨10.1007/978-3-319-89366-2_15⟩
Lecture Notes in Computer Science ISBN: 9783319893655
FoSSaCS
International audience; We define a variant of realizability where realizers are pairs of a term and a substitution. This variant allows us to prove the normalization of a simply-typed call-by-need λ-calculus with control due to Ariola et al. Indeed
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::aac9d5cf3c09a69aa185d45683abe0ab
https://hal.inria.fr/hal-01624839
https://hal.inria.fr/hal-01624839
Publikováno v:
Technologies logicielles Architectures des systèmes.
Un assistant de preuve est un logiciel interactif permettant a son utilisateur de construire des demonstrations de facon semi-automatique, tout en garantissant la correction de ces demonstrations. Ce type d'outil est particulierement utile a la verif
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::97017f94cc22575f7335276aca7bb8ba
https://doi.org/10.51257/a-v1-h3310
https://doi.org/10.51257/a-v1-h3310
Autor:
Théo Zimmermann, Hugo Herbelin
Publikováno v:
Type Theory Based Tools
Type Theory Based Tools, Jan 2017, Paris, France
HAL
Type Theory Based Tools, Jan 2017, Paris, France
HAL
International audience; We report on a work-in-progress to re-implement Coq's apply tactic in order to embed some form of simple automation. We design it in a declarative way, relying on typeclasses eauto, a tactic which gives access to the proof-sea
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::d273499a34f484b4a4bad0e5506db558
https://hal.archives-ouvertes.fr/hal-01671994/document
https://hal.archives-ouvertes.fr/hal-01671994/document
Autor:
Hugo Herbelin, Zena M. Ariola
Publikováno v:
Journal of Functional Programming. 18:373-419
The historical design of the call-by-value theory of control relies on the reification of evaluation contexts as regular functions and on the use of ordinary term application for jumping to a continuation. To the contrary, thecontrol calculus, develo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::20b11dd0b2618e7eb24f1a7bf23a9dfc
https://doi.org/10.1017/s0956796807006612
https://doi.org/10.1017/s0956796807006612
Publikováno v:
Higher-Order and Symbolic Computation
Higher-Order and Symbolic Computation, Springer Verlag, 2007
Higher-Order and Symbolic Computation, 2007
Higher-Order and Symbolic Computation, Springer Verlag, 2007
Higher-Order and Symbolic Computation, 2007
International audience; There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters, the continuations become composable and the calculi become more expres
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a7b749f4f5c0e5400181ca87ac5c763e
https://doi.org/10.1007/s10990-007-9006-0
https://doi.org/10.1007/s10990-007-9006-0
Autor:
Hugo Herbelin
Publikováno v:
Mathematical Structures in Computer Science
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2015, From type theory and homotopy theory to Univalent Foundations of Mathematics, 25 (Special issue 05), pp.16. ⟨10.1017/S0960129514000528⟩
Mathematical Structures in Computer Science, 2015, From type theory and homotopy theory to Univalent Foundations of Mathematics, 25 (Special issue 05), pp.16. ⟨10.1017/S0960129514000528⟩
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2015, From type theory and homotopy theory to Univalent Foundations of Mathematics, 25 (Special issue 05), pp.16. ⟨10.1017/S0960129514000528⟩
Mathematical Structures in Computer Science, 2015, From type theory and homotopy theory to Univalent Foundations of Mathematics, 25 (Special issue 05), pp.16. ⟨10.1017/S0960129514000528⟩
International audience; This paper presents a dependently-typed construction of semi-simplicial sets in type theory where sets are taken to be types. This addresses an open question raised on the wiki of the special year on Univalent Foundations at t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::fb4ba7a993dc26e3d82849222b0fda3f
https://hal.inria.fr/hal-00935446
https://hal.inria.fr/hal-00935446
Publikováno v:
ICFP
There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters (prompts), the continuations become composable and the calculi are believed to become more expr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::32ec80f45771b8434798c16d1fd62b5e
https://doi.org/10.1145/1016848.1016860
https://doi.org/10.1145/1016848.1016860