We gratefully acknowledge support from
the Simons Foundation and member institutions.

Logic in Computer Science

Authors and titles for cs.LO in Jan 2021

[ total of 107 entries: 1-50 | 51-100 | 101-107 ]
[ showing 50 entries per page: fewer | more | all ]
[1]  arXiv:2101.00102 [pdf, other]
Title: Verifying a Cruise Control System using Simulink and SpaceEx
Authors: Nikolaos Kekatos
Subjects: Logic in Computer Science (cs.LO); Systems and Control (eess.SY)
[2]  arXiv:2101.00956 [pdf, ps, other]
Title: Computable Random Variables and Conditioning
Authors: Pieter Collins
Comments: arXiv admin note: text overlap with arXiv:1409.4667
Subjects: Logic in Computer Science (cs.LO); Probability (math.PR)
[3]  arXiv:2101.00958 [pdf, other]
Title: Scalable Online Conformance Checking Using Incremental Prefix-Alignment Computation
Subjects: Logic in Computer Science (cs.LO); Software Engineering (cs.SE)
[4]  arXiv:2101.00992 [pdf, other]
Title: Formal Game Grammar and Equivalence
Comments: 8 pages, 7 figures. Presented at the 2020 IEEE Conference on Games (Full Paper. August 24-27, 2020). arXiv admin note: text overlap with arXiv:1912.03295
Journal-ref: 2020 IEEE Conference on Games (CoG), Osaka, Japan, 2020, pp. 206-213
Subjects: Logic in Computer Science (cs.LO)
[5]  arXiv:2101.01676 [pdf, ps, other]
Title: Dynamic Preference Logic meets Iterated Belief Change: Representation Results and Postulates Characterization
Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI)
[6]  arXiv:2101.01842 [pdf, other]
Title: Confluence up to Garbage in Graph Transformation
Comments: 33 pages, 2021
Subjects: Logic in Computer Science (cs.LO)
[7]  arXiv:2101.01944 [pdf, ps, other]
Title: Logics of First-Order Constraints -- A Category Independent Approach
Authors: Uwe Wolter
Comments: 23 pages, presented at the 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019), London, UK, June 3-6, 2019
Subjects: Logic in Computer Science (cs.LO); Software Engineering (cs.SE)
[8]  arXiv:2101.02690 [pdf]
Title: Theorem Proving and Algebra
Authors: Joseph A. Goguen
Comments: 427+ xviii pages, 38 figures, Unfinished book by Joseph A. Goguen, Edited by Kokichi Futatsugi, Narciso Mart\'i-Oliet and Jos\'e Meseguer; revised version corrects some strange characters in page xv
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL); Symbolic Computation (cs.SC)
[9]  arXiv:2101.02835 [html]
Title: Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
Authors: Claudio Sacerdoti Coen (University of Bologna), Alwen Tiu (The Australian National University)
Journal-ref: EPTCS 332, 2021
Subjects: Logic in Computer Science (cs.LO)
[10]  arXiv:2101.02994 [pdf, other]
Title: Quotients, inductive types, and quotient inductive types
Subjects: Logic in Computer Science (cs.LO)
[11]  arXiv:2101.03113 [pdf, ps, other]
Title: A Rewriting Logic Approach to Specification, Proof-search, and Meta-proofs in Sequent Systems
Subjects: Logic in Computer Science (cs.LO); Logic (math.LO)
[12]  arXiv:2101.03215 [pdf, ps, other]
Title: Polymorphic System I
Comments: 20 pages plus appendix
Journal-ref: In IFL 2020: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages (IFL 2020). Association for Computing Machinery, New York, NY, USA, 127-137
Subjects: Logic in Computer Science (cs.LO)
[13]  arXiv:2101.03591 [pdf, ps, other]
Title: Tietze Equivalences as Weak Equivalences
Subjects: Logic in Computer Science (cs.LO); Algebraic Topology (math.AT)
[14]  arXiv:2101.03807 [pdf, ps, other]
Title: Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading
Comments: In Proceedings LFMTP 2020, arXiv:2101.02835
Journal-ref: EPTCS 332, 2021, pp. 1-17
Subjects: Logic in Computer Science (cs.LO)
[15]  arXiv:2101.03808 [pdf, other]
Title: Object-Level Reasoning with Logics Encoded in HOL Light
Authors: Petros Papapanagiotou (University of Edinburgh), Jacques Fleuriot (University of Edinburgh)
Comments: In Proceedings LFMTP 2020, arXiv:2101.02835
Journal-ref: EPTCS 332, 2021, pp. 18-34
Subjects: Logic in Computer Science (cs.LO); Symbolic Computation (cs.SC)
[16]  arXiv:2101.03809 [pdf, other]
Title: Deductive Systems and Coherence for Skew Prounital Closed Categories
Comments: In Proceedings LFMTP 2020, arXiv:2101.02835
Journal-ref: EPTCS 332, 2021, pp. 35-53
Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT)
[17]  arXiv:2101.03810 [pdf, ps, other]
Title: Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory
Authors: Bruno Barras (Inria, Université Paris-Saclay, ENS Paris-Saclay, CNRS, LSV, Gif-sur-Yvette, France), Valentin Maestracci (Université Paris-Saclay, ENS Paris-Saclay, CNRS, LSV, Gif-sur-Yvette, France)
Comments: In Proceedings LFMTP 2020, arXiv:2101.02835
Journal-ref: EPTCS 332, 2021, pp. 54-67
Subjects: Logic in Computer Science (cs.LO)
[18]  arXiv:2101.03866 [pdf, other]
Title: Register Automata with Extrema Constraints, and an Application to Two-Variable Logic
Comments: The short version of this article appeared in the conference proceedings of LICS 2020
Subjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL)
[19]  arXiv:2101.04819 [pdf, ps, other]
Title: Parametricity for Nested Types and GADTs
Subjects: Logic in Computer Science (cs.LO)
[20]  arXiv:2101.04971 [pdf, ps, other]
Title: An Algebraic Method to Fidelity-based Model Checking over Quantum Markov Chains
Authors: Ming Xu (1), Jianling Fu (1), Jingyi Mei (1), Yuxin Deng (1) ((1) Shanghai Key Lab of Trustworthy Computing, East China Normal University, Shanghai, China)
Subjects: Logic in Computer Science (cs.LO)
[21]  arXiv:2101.05024 [pdf]
Title: Proposal for Adding Useful Features to Petri-Net Model Checkers
Authors: Hubert Garavel (CONVECS)
Subjects: Logic in Computer Science (cs.LO)
[22]  arXiv:2101.05140 [pdf, other]
Title: Secure Process Algebra
Authors: Yong Wang
Comments: 172 pages, 36 figures, 28 tables
Subjects: Logic in Computer Science (cs.LO); Cryptography and Security (cs.CR)
[23]  arXiv:2101.05256 [html]
Title: Proceedings 6th International Workshop on Symbolic-Numeric methods for Reasoning about CPS and IoT
Authors: Thao Dang (Verimag/CNRS, France), Stefan Ratschan (Institute of Computer Science, Czech Academy of Sciences)
Journal-ref: EPTCS 331, 2021
Subjects: Logic in Computer Science (cs.LO); Symbolic Computation (cs.SC)
[24]  arXiv:2101.05257 [pdf, ps, other]
Title: Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
Comments: 23 pages. Submitted for publication
Subjects: Logic in Computer Science (cs.LO); Logic (math.LO)
[25]  arXiv:2101.05415 [pdf, other]
Title: Analysis of E-commerce Ranking Signals via Signal Temporal Logic
Authors: Tommaso Dreossi (Amazon Search), Giorgio Ballardin (Amazon Search), Parth Gupta (Amazon Search), Jan Bakus (Amazon Search), Yu-Hsiang Lin (Amazon Search), Vamsi Salaka (Amazon Search)
Comments: In Proceedings SNR 2020, arXiv:2101.05256
Journal-ref: EPTCS 331, 2021, pp. 33-42
Subjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL); Information Retrieval (cs.IR); Machine Learning (cs.LG)
[26]  arXiv:2101.05678 [pdf, other]
Title: Lebesgue integration. Detailed proofs to be formalized in Coq
Authors: François Clément (SERENA, CERMICS), Vincent Martin (LMAC)
Subjects: Logic in Computer Science (cs.LO); Classical Analysis and ODEs (math.CA); Functional Analysis (math.FA)
[27]  arXiv:2101.05754 [pdf, other]
Title: A Strong Bisimulation for a Classical Term Calculus by Means of Multiplicative and Exponential Reduction
Comments: arXiv admin note: text overlap with arXiv:1906.09370
Subjects: Logic in Computer Science (cs.LO)
[28]  arXiv:2101.06087 [pdf, ps, other]
Title: An Abstract Contract Theory for Programs with Procedures
Authors: Christian Lidström, Dilian Gurov (KTH Royal Institute of Technology, Stockholm, Sweden)
Comments: 24 pages. This is the full version of the paper An Abstract Contract Theory for Programs with Procedures, published in Proceedings of the 24th International Conference on Fundamental Approaches to Software Engineering (FASE 2021), which includes the proofs of all theorems and additional examples. The conference version should always be cited
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
[29]  arXiv:2101.06195 [pdf, other]
Title: Switched Systems as Hybrid Programs
Comments: Long version of paper at ADHS 2021 (7th IFAC Conference on Analysis and Design of Hybrid Systems, July 7-9, 2021)
Subjects: Logic in Computer Science (cs.LO); Systems and Control (eess.SY)
[30]  arXiv:2101.06825 [pdf, other]
Title: Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
Comments: 30 pages, 2 figures, 2 tables, extended version of paper that appeared in International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2021, invited to Logical Methods in Computer Science journal, Version Updates: Notable changes include a self-comparison with different options in Section 7, and Section 6, which discusses implementation details of the prototype
Subjects: Logic in Computer Science (cs.LO)
[31]  arXiv:2101.07066 [pdf, other]
Title: Reversible Computation in Petri Nets
Authors: Kyriaki Psara
Comments: PhD dissertation
Subjects: Logic in Computer Science (cs.LO)
[32]  arXiv:2101.07109 [pdf, ps, other]
Title: Efficient Monitoring of Hyperproperties using Prefix Trees
Comments: arXiv admin note: text overlap with arXiv:1807.00758, arXiv:1906.00798
Subjects: Logic in Computer Science (cs.LO)
[33]  arXiv:2101.07161 [pdf, other]
Title: Realizing Omega-regular Hyperproperties
Comments: International Conference on Computer Aided Verification (CAV 2020)
Journal-ref: =In: Lahiri S., Wang C. (eds) Computer Aided Verification. CAV 2020. Lecture Notes in Computer Science, vol 12225
Subjects: Logic in Computer Science (cs.LO)
[34]  arXiv:2101.07232 [pdf, other]
Title: Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications
Subjects: Logic in Computer Science (cs.LO); Hardware Architecture (cs.AR)
[35]  arXiv:2101.07491 [pdf, ps, other]
Title: Automated Verification and Synthesis of Stochastic Hybrid Systems: A Survey
Subjects: Logic in Computer Science (cs.LO); Systems and Control (eess.SY)
[36]  arXiv:2101.07700 [pdf, ps, other]
Title: Proof Automation in the Theory of Finite Sets and Finite Set Relation Algebra
Subjects: Logic in Computer Science (cs.LO)
[37]  arXiv:2101.07711 [pdf, ps, other]
Title: On the Decidability of Behavioral Equivalences for (P,P)-PRS
Authors: Irina Lomazova (HSE University, Moscow, Russia), Vladimir Bashkin (Yaroslavl State University, Yaroslavl, Russia)
Comments: Submitted to LICS'2021
Subjects: Logic in Computer Science (cs.LO)
[38]  arXiv:2101.07758 [pdf, other]
Title: A bi-directional extensible interface between Lean and Mathematica
Comments: arXiv admin note: substantial text overlap with arXiv:1712.09288
Subjects: Logic in Computer Science (cs.LO); Mathematical Software (cs.MS)
[39]  arXiv:2101.07761 [pdf, other]
Title: The Coq Proof Script Visualiser (coq-psv)
Authors: Mario Frank
Comments: This contribution was presented during a talk at the Coq Workshop 2020, affiliated with the IJCAR 2020
Subjects: Logic in Computer Science (cs.LO); Computers and Society (cs.CY)
[40]  arXiv:2101.07847 [pdf, other]
Title: The Complexity of Monitoring Hyperproperties
Subjects: Logic in Computer Science (cs.LO)
[41]  arXiv:2101.08184 [pdf, other]
Title: Fixpoint Theory -- Upside Down
Subjects: Logic in Computer Science (cs.LO)
[42]  arXiv:2101.08257 [pdf, ps, other]
Title: Program Repair for Hyperproperties
Comments: arXiv admin note: text overlap with arXiv:2101.07847
Subjects: Logic in Computer Science (cs.LO)
[43]  arXiv:2101.08364 [pdf, ps, other]
Title: Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic (long version)
Subjects: Logic in Computer Science (cs.LO)
[44]  arXiv:2101.08377 [pdf, other]
Title: Finite Model Theory of the Triguarded Fragment and Related Logics
Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Computational Complexity (cs.CC); Logic (math.LO)
[45]  arXiv:2101.08491 [pdf, ps, other]
Title: Complete trace models of state and control
Authors: Guilhem Jaber (GALLINETTE, LS2N), Andrzej S. Murawski
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
[46]  arXiv:2101.08735 [pdf, ps, other]
Title: Work-sensitive Dynamic Complexity of Formal Languages
Subjects: Logic in Computer Science (cs.LO); Computational Complexity (cs.CC); Data Structures and Algorithms (cs.DS)
[47]  arXiv:2101.08880 [pdf, ps, other]
Title: Controller Synthesis for Hyperproperties
Comments: arXiv admin note: text overlap with arXiv:2101.08257
Subjects: Logic in Computer Science (cs.LO)
[48]  arXiv:2101.09042 [pdf, ps, other]
Title: PEQcheck: Localized and Context-aware Checking of Functional Equivalence (Technical Report)
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
[49]  arXiv:2101.09655 [pdf, ps, other]
Title: Relational Type Theory (All Proofs)
Subjects: Logic in Computer Science (cs.LO)
[50]  arXiv:2101.10166 [pdf]
Title: The Agda Universal Algebra Library and Birkhoff's Theorem in Dependent Type Theory
Authors: William DeMeo
Comments: 111 pages
Subjects: Logic in Computer Science (cs.LO); Logic (math.LO)
[ total of 107 entries: 1-50 | 51-100 | 101-107 ]
[ showing 50 entries per page: fewer | more | all ]

Disable MathJax (What is MathJax?)

Links to: arXiv, form interface, find, cs, 2110, contact, help  (Access key information)