Zobrazeno 1 - 10
of 155
pro vyhledávání: '"Theory of computation ��� Logic and verification"'
We investigate expansions of Presburger arithmetic (Pa), i.e., the theory of the integers with addition and order, with additional structure related to exponentiation: either a function that takes a number to the power of 2, or a predicate 2^ℕ for
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8283c6be4cc6d7a05e2999127224345e
http://arxiv.org/abs/2305.03037
http://arxiv.org/abs/2305.03037
Autor:
Ivanov, Ievgen
We propose a generalization of Newman’s lemma which gives a criterion of confluence for a wide class of not-necessarily-terminating abstract rewriting systems. We show that ordinary Newman’s lemma for terminating systems can be considered as a co
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d7261ff881800e41c0c2fa792ee542a6
Over-approximating (OX) program logics, such as separation logic (SL), are used for verifying properties of heap-manipulating programs: all terminating behaviour is characterised, but established results and errors need not be reachable. OX function
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::00193445dbb70cf26180e88cfae381e0
In the process of designing a computer system S and checking whether an abstract model ℳ of S verifies a given specification property η, one might have only a partial knowledge of the model, either because ℳ has not yet been completely defined (
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e3bc73fed69b1f27587f542a1d534ade
Autor:
Fernández, Maribel
In this talk we discuss the nominal approach to the specification of languages with binders and some applications to programming languages and verification.
LIPIcs, Vol. 260, 8th International Conference on Formal Structures for Computation and
LIPIcs, Vol. 260, 8th International Conference on Formal Structures for Computation and
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b9528b12f6c816eba13d78b90b61ae63
Autor:
Kirst, Dominik, Peters, Benjamin
Gödel published his groundbreaking first incompleteness theorem in 1931, stating that a large class of formal logics admits independent sentences which are neither provable nor refutable. This result, in conjunction with his second incompleteness th
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3f6f63d6692e730f0e796daaaa47f5f6
This report documents the program and the outcomes of Dagstuhl Seminar 22411 "Theory and Practice of SAT and Combinatorial Solving". The purpose of this workshop was to explore the Boolean satisfiability (SAT) problem, which plays a fascinating dual
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::234ba046fbad6ad0d1e8f1bd9e4895d4
We introduce a variation on Barthe et al.’s higher-order logic in which formulas are interpreted as predicates over open rather than closed objects. This way, concepts which have an intrinsically functional nature, like continuity, differentiabilit
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1392404bed30845df71b928c52674ea3
Typestates are a notion of behavioral types that describe protocols for stateful objects, specifying the available methods for each state. Ensuring methods are called in the correct order (protocol compliance), and that, if and when the program termi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::841483966868020d20b2015e2cf54171
Autor:
van der Weide, Niels
We develop the formal theory of monads, as established by Street, in univalent foundations. This allows us to formally reason about various kinds of monads on the right level of abstraction. In particular, we define the bicategory of monads internal
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1c89abb89c267f0d8432c5dd0887cf1c
http://arxiv.org/abs/2212.08515
http://arxiv.org/abs/2212.08515