We provide a sound and relatively complete Hoare-like proof system for
reasoning about partial correctness of recursive procedures in presence of
local variables and the call-by-value parameter mechanism, and in which the
correctness proofs are linear in the length of the program. We argue that in
spite of the fact that Hoare-like proof systems for recursive procedures were
intensively studied, no such proof system has been proposed in the literature.

more |
pdf
| html
None.

None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 0

Unqiue Words: 0

Multiparty sessions are systems of concurrent processes, which allow several
participants to communicate by sending and receiving messages. Their overall
behaviour can be described by means of global types. Typable multiparty session
enjoy lock-freedom. We look at multiparty sessions as open systems by a
suitable definition of connection transforming compatible processes into
gateways (forwarders). A relation resembling the standard subtyping relation
for session types is used to formalise compatibility. We show that the session
obtained by connection can be typed by manipulating the global types of the
starting sessions. This allows us to prove that lock-freedom is preserved by
connection.

more |
pdf
| html
None.

None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 0

Unqiue Words: 0

The tractability conjecture for finite domain Constraint Satisfaction
Problems (CSPs) stated that such CSPs are solvable in polynomial time whenever
there is no natural reduction, in some precise technical sense, from the 3-SAT
problem; otherwise, they are NP-complete. Its recent resolution draws on an
algebraic characterization of the conjectured borderline: the CSP of a finite
structure permits no natural reduction from 3-SAT if and only if the stabilizer
of the polymorphism clone of the core of the structure satisfies some
nontrivial system of identities, and such satisfaction is always witnessed by
several specific nontrivial systems of identities which do not depend on the
structure.
The tractability conjecture has been generalized in the above formulation to
a certain class of infinite domain CSPs, namely, CSPs of reducts of finitely
bounded homogeneous structures. It was subsequently shown that the conjectured
borderline between hardness and tractability, i.e., a natural reduction from
3-SAT, can be characterized for this...

more |
pdf
| html
None.

None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 0

Unqiue Words: 0

Assert is a website where the best academic papers on arXiv (computer science, math, physics), bioRxiv (biology), BITSS (reproducibility), EarthArXiv (earth science), engrXiv (engineering), LawArXiv (law), PsyArXiv (psychology), SocArXiv (social science), and SportRxiv (sport research) bubble to the top each day.

Papers are scored (in real-time) based on how verifiable they are (as determined by their Github repos) and how interesting they are (based on Twitter).

To see top papers, follow us on twitter @assertpub_ (arXiv), @assert_pub (bioRxiv), and @assertpub_dev (everything else).

To see beautiful figures extracted from papers, follow us on Instagram.

*Tracking 189,567 papers.*

Sort results based on if they are interesting or reproducible.

Interesting

Reproducible