Search Results - programming language theory

  1. 81
  2. 82
  3. 83
  4. 84
  5. 85
  6. 86
  7. 87
  8. 88
  9. 89
  10. 90
  11. 91
  12. 92
  13. 93
  14. 94
  15. 95

    Automated Deduction - CADE 28 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings /

    Published 2021
    Table of Contents: “…Static EL Tboxes -- Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance -- A Unifying Splitting Framework -- Integer Induction in Saturation -- Superposition with First-Class Booleans and Inprocessing Clausification -- Superposition for Full Higher-Order Logic -- Implementation and Application -- Making Higher-Order Superposition Work -- Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver -- Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant -- An Automated Approach to the Collatz Conjecture -- Verified Interactive Computation of Definite Integrals -- ATP and AI -- Confidences for Commonsense Reasoning -- Neural Precedence Recommender -- Improving ENIGMA-Style Clause Selection While Learning From History -- System Descriptions -- A Normative Supervisor for Reinforcement Learning Agents (System Description) -- Automatically Building Diagrams for Olympiad Geometry Problems (System Description) -- The Fusemate Logic Programming System (System Description) -- Twee: An Equational Theorem Prover (System Description) -- The Isabelle/Naproche Natural Language Proof Assistant (System Description) -- The Lean 4 Theorem Prover and Programming Language (System Description) -- Harpoon: Mechanizing Metatheory Interactively (System Description).…”
    Link to Metadata
    Electronic eBook
  16. 96

    Automated Deduction - CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings /

    Published 2023
    Table of Contents: “…Certified Core-Guided MaxSAT Solving -- Superposition with Delayed Unification -- On Incremental Pre-processing for SMT -- Verified Given Clause Procedures -- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment -- Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs -- An Isabelle/HOL Formalization of the SCL(FOL) Calculus -- SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning -- Formal Reasoning about Influence in Natural Sciences Experiments -- A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification) -- SAT-Based Subsumption Resolution -- A more Pragmatic CDCL for IsaSAT and targetting LLVM (Short Paper) -- Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper) -- COOL 2 - A Generic Reasoner for Modal Fixpoint Logics (System Description) -- Choose your Colour: Tree Interpolation for Quantified Formulas in SMT -- Proving Termination of C Programs with Lists -- Reasoning about Regular Properties: A Comparative Study -- Program Synthesis in Saturation -- A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus -- Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs -- Verification of NP-hardness Reduction Functions for Exact Lattice Problems -- Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic -- Left-Linear Completion with AC Axioms -- On P -interpolation in local theory extensions and applications to the study of interpolation in the description logics EL, EL+ -- Theorem Proving in Dependently-Typed Higher-Order Logic -- Towards Fast Nominal Anti-Unification of Letrec-Expressions -- Confluence Criteria for Logically Constrained Rewrite Systems -- Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory -- An Experimental Pipeline for Automated Reasoning in Natural Language (Short paper) -- Combining Combination Properties: An Analysis of Stable-infiniteness, Convexity, and Politeness -- Decidability of difference logic over the reals with uninterpreted unary predicates -- Incremental Rewriting Modulo SMT -- Iscalc: an Interactive Symbolic Computation Framework (System Description).…”
    Link to Metadata
    Electronic eBook
  17. 97
  18. 98
  19. 99

    Computer Aided Verification 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II /

    Published 2019
    Subjects: “…Formal Languages and Automata Theory.…”
    Link to Metadata
    Electronic eBook
  20. 100

    Foundations of Software Science and Computation Structures 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Sof...

    Published 2019
    Table of Contents: “…Universal Graphs and Good for Small Games Automata: New Tools for Infinite Duration Games -- Resource-Tracking Concurrent Games -- Change Actions: Models of Generalised Differentiation -- Coalgebra Learning via Duality -- Tight Worst-Case Bounds for Polynomial Loop Programs -- A Complete Normal-Form Bisimilarity for State -- Identifiers in Registers - Describing Network Algorithms with Logic -- The Impatient May Use Limited Optimism to Minimize Regret -- Causality in Linear Logic: Full Completeness and Injectivity (Unit-Free Multiplicative-Additive Fragment) -- Rewriting Abstract Structures: Materialization Explained Categorically -- Two-Way Parikh Automata with a Visibly Pushdown Stack -- Kleene Algebra with Hypotheses -- Trees in Partial Higher Dimensional Automata -- The Bernays-Schoenfinkel-Ramsey Class of Separation Logic on Arbitrary Domains -- Continuous Reachability for Unordered Data Petri Nets is in PTime -- Optimal Satisfiability Checking for Arithmetic mu-Calculi -- Constructing Inductive-Inductive Types in Cubical Type Theory -- Causal Inference by String Diagram Surgery -- Higher-Order Distributions for Differential Linear Logic -- Languages Ordered by the Subword Order -- Strong Adequacy and Untyped Full-Abstraction for Probabilistic Coherence Spaces -- A Sound and Complete Logic for Algebraic Effects -- Equational Axiomatization of Algebras with Structure -- Towards a Structural Proof Theory of Probabilistic μ-Calculi -- Partial and Conditional Expectations in Markov Decision Processes with Integer Weights -- Equational Theories and Monads from Polynomial Cayley Representations -- A Dialectica-Like Interpretation of a Linear MSO on Infinite Words -- Deciding Equivalence of Separated Non-Nested Attribute Systems in Polynomial Time -- Justness: A Completeness Criterion for Capturing Liveness Properties -- Path category for Free - Open Morphisms from Coalgebras with Non-Deterministic Branching.…”
    Link to Metadata
    Electronic eBook