Logic in Computer Science
New submissions
[ showing up to 2000 entries per page: fewer  more ]
New submissions for Mon, 2 Aug 21
 [1] arXiv:2107.14283 [pdf, ps, other]

Title: Syllepsis in Homotopy Type TheoryAuthors: Kristina SojakovaSubjects: Logic in Computer Science (cs.LO)
It is wellknown that in homotopy type theory (HoTT), one can prove the EckmannHilton theorem: given two 2loops p, q : 1 = 1 on the reflexivity path at an arbitrary point a : A, we have pq = qp. If we go one dimension higher, i.e., if p and q are 3loops, we show that a property classically known as syllepsis also holds in HoTT: namely, the EckmannHilton proof for q and p is the inverse of the EckmannHilton proof for p and q.
 [2] arXiv:2107.14487 [pdf, other]

Title: Refining Labelled Systems for Modal and Constructive Logics with ApplicationsAuthors: Tim LyonComments: PhD ThesisSubjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Discrete Mathematics (cs.DM); Formal Languages and Automata Theory (cs.FL); Logic (math.LO)
This thesis introduces the "method of structural refinement", which serves as a means of transforming the relational semantics of a modal and/or constructive logic into an 'economical' proof system by connecting two prooftheoretic paradigms: labelled and nested sequent calculi. The formalism of labelled sequents has been successful in that cutfree calculi in possession of desirable prooftheoretic properties can be automatically generated for large classes of logics. Despite these qualities, labelled systems make use of a complicated syntax that explicitly incorporates the semantics of the associated logic, and such systems typically violate the subformula property to a high degree. By contrast, nested sequent calculi employ a simpler syntax and adhere to a strict reading of the subformula property, making such systems useful in the design of automated reasoning algorithms. However, the downside of the nested sequent paradigm is that a general theory concerning the automated construction of such calculi (as in the labelled setting) is essentially absent, meaning that the construction of nested systems and the confirmation of their properties is usually done on a casebycase basis. The refinement method connects both paradigms in a fruitful way, by transforming labelled systems into nested (or, refined labelled) systems with the properties of the former preserved throughout the transformation process.
To demonstrate the method of refinement and some of its applications, we consider grammar logics, firstorder intuitionistic logics, and deontic STIT logics. The introduced refined labelled calculi will be used to provide the first proofsearch algorithms for deontic STIT logics. Furthermore, we employ our refined labelled calculi for grammar logics to show that every logic in the class possesses the effective Lyndon interpolation property.  [3] arXiv:2107.14651 [pdf, ps, other]

Title: Minimal Translations from Synchronous Communication to Synchronizing Locks (Extended Version)Subjects: Logic in Computer Science (cs.LO)
In order to understand the relative expressive power of larger concurrent programming languages, we analyze translations of small process calculi which model the communication and synchronization of concurrent processes. The source language SYNCSIMPLE is a minimalistic model for message passing concurrency while the target language LOCKSIMPLE is a minimalistic model for shared memory concurrency. The former is a calculus with synchronous communication of processes, while the latter has synchronizing mutable locations  called locks  that behave similarly to binary semaphores. The criteria for correctness of translations is that they preserve and reflect maytermination and musttermination of the processes. We show that there is no correct compositional translation from SYNCSIMPLE to LOCKSIMPLE that uses one or two locks, independent from the initialisation of the locks. We also show that there is a correct translation that uses three locks. Also variants of the locks are taken into account with different blocking behavior.
 [4] arXiv:2107.14668 [pdf, ps, other]

Title: Interleaving & Reconfigurable Interaction: Separating Choice from Scheduling using GlueComments: This work is funded by the ERC consolidator grant DSynMA (No. 772459) and the Swedish research council grants: SynTM (No.202003401) and VR project (No. 202004963)Subjects: Logic in Computer Science (cs.LO)
Reconfigurable interaction induces another dimension of nondeterminism in concurrent systems which makes it hard to reason about the different choices of the system from a global perspective. Namely, (1) choices that correspond to concurrent execution of independent events; and (2) forced interleaving (or scheduling) due to reconfiguration. Unlike linear order semantics of computations, partial order semantics recovers information about the interdependence among the different events for fixed interaction, but still is unable to handle reconfiguration. We introduce glued partial orders as a way to capture reconfiguration. Much like partial orders capture all possible choices for fixed systems, glued partial orders capture all possible choices alongside reconfiguration. We show that a glued partial order is sufficient to correctly capture all partial order computations that differ in forced interleaving due to reconfiguration. Furthermore, we show that computations belonging to different glued partial orders are only different due to nondeterminism.
Crosslists for Mon, 2 Aug 21
 [5] arXiv:2107.14325 (crosslist from cs.CR) [pdf]

Title: PiBase: An IoTbased Security System using Raspberry Pi and Google FirebaseSubjects: Cryptography and Security (cs.CR); Computer Vision and Pattern Recognition (cs.CV); Logic in Computer Science (cs.LO)
Smart environments are environments where digital devices are connected to each other over the Internet and operate in sync. Security is of paramount importance in such environments. This paper addresses aspects of authorized access and intruder detection for smart environments. Proposed is PiBase, an Internet of Things (IoT)based app that aids in detecting intruders and providing security. The hardware for the application consists of a Raspberry Pi, a PIR motion sensor to detect motion from infrared radiation in the environment, an Android mobile phone and a camera. The software for the application is written in Java, Python and NodeJS. The PIR sensor and Pi camera module connected to the Raspberry Pi aid in detecting human intrusion. Machine learning algorithms, namely Haarfeature based cascade classifiers and Linear Binary Pattern Histograms (LBPH), are used for face detection and face recognition, respectively. The app lets the user create a list of nonintruders and anyone that is not on the list is identified as an intruder. The app alerts the user only in the event of an intrusion by using the Google Firebase Cloud Messaging service to trigger a notification to the app. The user may choose to add the detected intruder to the list of nonintruders through the app to avoid further detections as intruder. Face detection by the Haar Cascade algorithm yields a recall of 94.6%. Thus, the system is both highly effective and relatively low cost.
 [6] arXiv:2107.14509 (crosslist from cs.DC) [pdf, other]

Title: On Strong Observational Refinement and Forward SimulationComments: Full version of the paper to appear in DISC 2021Subjects: Distributed, Parallel, and Cluster Computing (cs.DC); Logic in Computer Science (cs.LO)
Hyperproperties are correctness conditions for labelled transition systems that are more expressive than traditional trace properties, with particular relevance to security. Recently, Attiya and Enea studied a notion of strong observational refinement that preserves all hyperproperties. They analyse the correspondence between forward simulation and strong observational refinement in a setting with finite traces only. We study this correspondence in a setting with both finite and infinite traces. In particular, we show that forward simulation does not preserve hyperliveness properties in this setting. We extend the forward simulation proof obligation with a progress condition, and prove that this progressive forward simulation does imply strong observational refinement.
 [7] arXiv:2107.14581 (crosslist from quantph) [pdf, ps, other]

Title: Causality in higher order process theoriesSubjects: Quantum Physics (quantph); Logic in Computer Science (cs.LO); Category Theory (math.CT)
Quantum supermaps provide a framework in which higher order quantum processes can act on lower order quantum processes. In doing so, they enable the definition and analysis of new quantum protocols and causal structures. Recently, the key features of quantum supermaps were captured through a general categorical framework, which when iterated yields the framework of higher order process theories (HOPT). The HOPT framework combines lower and higher order transformations in a single unified theory, with its mathematical structure shown to coincide with the notion of a closed monoidal category. Here we provide an equivalent construction of the HOPT framework from four simple axioms of processtheoretic nature. We then use the HOPT framework to establish connections between foundational features such as causality, determinism, and signalling, and to explore their interaction with the mathematical structure of *autonomy.
Replacements for Mon, 2 Aug 21
 [8] arXiv:1811.04196 (replaced) [pdf]

Title: A Domain Theory for Statistical Probabilistic ProgrammingJournalref: Proc. ACM Program. Lang. 3(POPL): 36:136:29 (2019)Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
 [9] arXiv:2004.11185 (replaced) [pdf, ps, other]

Title: Proof Theory of Riesz Spaces and Modal Riesz SpacesSubjects: Logic in Computer Science (cs.LO)
 [10] arXiv:2103.05674 (replaced) [pdf, other]

Title: Synthesizing computable functions from rational specifications over infinite wordsSubjects: Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO)
 [11] arXiv:2105.10362 (replaced) [pdf, other]

Title: Functionals in the Clouds: An abstract architecture of serverless CloudNative AppsComments: improved version for submission to UCC 2021Subjects: Computation and Language (cs.CL); Logic in Computer Science (cs.LO)
[ showing up to 2000 entries per page: fewer  more ]
Disable MathJax (What is MathJax?)
Links to: arXiv, form interface, find, cs, recent, 2108, contact, help (Access key information)