Zobrazeno 1 - 10
of 70
pro vyhledávání: '"ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS"'
Autor:
Seiller, Thomas
The author introduced models of linear logic known as ''Interaction Graphs'' which generalise Girard's various geometry of interaction constructions. In this work, we establish how these models essentially rely on a deep connection between zeta funct
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0572acffc808d0c23c1de1b415b6971d
https://hal.science/hal-02458330
https://hal.science/hal-02458330
Publikováno v:
Ellipses, 2020, 9782340042612
National audience; Cet ouvrage débute par une introduction à la logique des prédicats du premier ordre : syntaxe, sémantique et preuves formelles. Il guide ensuite le lecteur vers quelques uns de ses aspects plus avancés : théorème de complét
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::0e60cb4554ffa7c4524730b4fba8d98a
https://hal.archives-ouvertes.fr/hal-02995890
https://hal.archives-ouvertes.fr/hal-02995890
Publikováno v:
International Workshop on Verification and Program Transformation
International Workshop on Verification and Program Transformation, Apr 2020, Dublin, Ireland. pp.110-124, ⟨10.4204/EPTCS.320.8⟩
[Research Report] LORIA UMR 7503 CNRS, INRIA, Université de LORRAINE. 2020, pp.36
VPT/HCVS@ETAPS
International Workshop on Verification and Program Transformation, Apr 2020, Dublin, Ireland. pp.110-124, ⟨10.4204/EPTCS.320.8⟩
[Research Report] LORIA UMR 7503 CNRS, INRIA, Université de LORRAINE. 2020, pp.36
VPT/HCVS@ETAPS
Distributed algorithms offer challenges in checking that they meet their specifications. Verification techniques can be extended to deal with the verification of safety properties of distributed algorithms. In this paper, we present an approach for c
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c72933bca1689ce7d9a4fbd4d4d1e91a
https://hal.inria.fr/hal-02997277
https://hal.inria.fr/hal-02997277
Autor:
Florian Rabe, Dennis Müller
Publikováno v:
LFMTP 2019 Logical Frameworks and Meta-Languages: Theory and Practice 2019
LFMTP 2019 Logical Frameworks and Meta-Languages: Theory and Practice 2019, Jun 2019, Vancouver, Canada
Electronic Proceedings in Theoretical Computer Science, Vol 307, Iss Proc. LFMTP 2019, Pp 40-54 (2019)
LFMTP@LICS
LFMTP 2019 Logical Frameworks and Meta-Languages: Theory and Practice 2019, Jun 2019, Vancouver, Canada
Electronic Proceedings in Theoretical Computer Science, Vol 307, Iss Proc. LFMTP 2019, Pp 40-54 (2019)
LFMTP@LICS
Logical frameworks are meta-formalisms in which the syntax and semantics of object logics and related formal systems can be defined. This allows object logics to inherit implementations from the framework including, e.g., parser, type checker, or mod
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6df4826a1a525a01ff732ed80dcfe2f1
https://hal.archives-ouvertes.fr/hal-02150167
https://hal.archives-ouvertes.fr/hal-02150167
Autor:
Colin Riba
This paper surveys a new perspective on tree automata and Monadic second-order logic (MSO) on infinite trees. We show that the operations on tree automata used in the translations of MSO-formulae to automata underlying Rabin’s Tree Theorem (the dec
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::cadf6016bf840ff9e0313c741a9cb17a
https://hal.science/hal-01261183v10/file/longproofs.pdf
https://hal.science/hal-01261183v10/file/longproofs.pdf
Autor:
Lescanne, Pierre, Bendkowski, Maciej
Publikováno v:
FSCD 2018
FSCD 2018, Jul 2018, Oxford, United Kingdom. ⟨10.4230/LIPIcs.FSCD.2018.11⟩
FSCD 2018, Jul 2018, Oxford, United Kingdom. ⟨10.4230/LIPIcs.FSCD.2018.11⟩
Environments and closures are two of the main ingredients of evaluation in lambda-calculus. A closure is a pair consisting of a lambda-term and an environment, whereas an environment is a list of lambda-terms assigned to free variables. In this paper
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c94293ecf6d15edbbaef6e0514cde589
https://hal-ens-lyon.archives-ouvertes.fr/ensl-01892406
https://hal-ens-lyon.archives-ouvertes.fr/ensl-01892406
Autor:
Rosemary Monahan, Dominique Méry
Publikováno v:
VPT@CAV
VPT 2013-First International Workshop on Verification and Program Transformation
VPT 2013-First International Workshop on Verification and Program Transformation, Alexei Lisitsa and Andrei Nemytykh, Jul 2013, Saint Petersburg, Russia. pp.57-73
VPT 2013-First International Workshop on Verification and Program Transformation
VPT 2013-First International Workshop on Verification and Program Transformation, Alexei Lisitsa and Andrei Nemytykh, Jul 2013, Saint Petersburg, Russia. pp.57-73
The refinement-based approach to developing software is based on thecorrect-by-construction paradigm were software systems are constructed via the step-by-step refinement of an initial high-level specification into a final concrete specification. Pro
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b5d0b57e354bd9b66a60fa02d9379dbc
https://doi.org/10.29007/9wm9
https://doi.org/10.29007/9wm9
Publikováno v:
ICDCN '18 Proceedings of the 19th International Conference on Distributed Computing and Networking
ICDCN 2018-19th International Conference on Distributed Computing and Networking
ICDCN 2018-19th International Conference on Distributed Computing and Networking, Jan 2018, Varanasi, India. pp.1-10, ⟨10.1145/3154273.3154321⟩
ICDCN
ICDCN 2018-19th International Conference on Distributed Computing and Networking
ICDCN 2018-19th International Conference on Distributed Computing and Networking, Jan 2018, Varanasi, India. pp.1-10, ⟨10.1145/3154273.3154321⟩
ICDCN
International audience; Swarms of mobile robots recently attracted the focus of the DistributedComputing community. One of the fundamental problemsin this context is that of exploration: the robots must coordinateto visit all locations that are reach
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a7751692fd3b7ca5bc436525a8e1c15c
https://hal.sorbonne-universite.fr/hal-01753439
https://hal.sorbonne-universite.fr/hal-01753439
Publikováno v:
Mathematical Structures in Computer Science
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2018, 28 (9), pp.1578--1605
Mathematical Structures in Computer Science, 2018, 28 (9), pp.1578--1605
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2018, 28 (9), pp.1578--1605
Mathematical Structures in Computer Science, 2018, 28 (9), pp.1578--1605
We present two extensions of theLFconstructive type theory featuring monadiclocks. A lock is a monadic type construct that captures the effect of anexternal call to an oracle. Such calls are the basic tool forplugging-inand gluing together, different
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::abd4b5bf3e199bd48ebd181296f1f404
http://hdl.handle.net/11390/1134891
http://hdl.handle.net/11390/1134891
Autor:
Michael Emmi, Constantin Enea
Publikováno v:
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2017
Proceedings of the ACM on Programming Languages, ACM, 2017
While many program properties like the validity of assertions and in-bounds array accesses admit nearly-trivial monitoring algorithms, the standard correctness criterion for concurrent data structures does not. Given an implementation of an arbitrary
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6be1fd7cc8b6cef24559cce754a96dd1
https://hal.archives-ouvertes.fr/hal-01943932/document
https://hal.archives-ouvertes.fr/hal-01943932/document