FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

This page contains an index consisting of author-provided keywords.

#
#SAT	(LaSh) Solving #SAT by Parameterized Algorithms: Exploiting Small Treewidth
#SMT(BV)	(IJCAR) A New Probabilistic Algorithm for Approximate Model Counting
#SMT(LA)	(PRUV) VolCE: An Efficient Tool for Solving #SMT(LA) Problems
2
2-CNF	(SAT) Minimal unsatisfiability and minimal strongly connected digraphs
A
A-infinity-(co)algebras	(HDRA) Minimal models for monomial algebras
abductive reasoning	(IJCAR) A Generic Framework for Implicate Generation Modulo Theories
Abella	(LFMTP) Functional programming with λ-tree syntax: a progress report (LFMTP) Computation-as-deduction in Abella: work in progress
ABNF	(VSTTE) A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
Absolute Correctness	(REFINE) Programming Without Refinement
abstract interpretation	(FM) Software Safety and Security and AI (SMT) Selfless Interpolation for Infinite-State Model Checking (LICS) Sound up-to techniques and Complete abstract domains (IJCAR) Checking Array Bounds by Abstract Interpretation and Symbolic Expressions (CSF) Inductive Invariants for Noninterference in Multi-agent Workflows (VSTTE) The Map Equality Domain (ICLP) An iterative approach to precondition inference using constrained Horn clauses (ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks (ICLP) Towards Incremental and Modular Context-sensitive Analysis
abstract recursion theory	(LCC) Computability over locally finite structures from algebra
abstract state machine	(DCM) Generic Graph Semantics
Abstract State Machines	(F-IDE) AsmetaF: a flattener for the ASMETA framework
Abstract syntax	(LFMTP) What Does This Notation Mean Anyway? BNF-style notation as it is actually used (LICS) Syntax and Semantics for Operations with Scopes
abstract winning condition	(SR) Concurrent games and semi-random determinacy
Abstraction	(CAV) Reasoning About TSO Programs Using Reduction and Abstraction (FM) Towards `Verifying' a Water Treatment System (ASPOCP) Towards Abstraction in ASP with an Application on Reasoning about Agent Policies (WST) Well-founded models in proofs of termination
abstraction learning	(LearnAut)
abstraction refinement	(CAV) Spacetime Interpolants (ICLP) An iterative approach to precondition inference using constrained Horn clauses
abstraction-refinement	(IJCAR) An abstraction-refinement framework for reasoning with large theories
accumulated weight constraints	(LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
Ackermann's Lemma	(IJCAR) FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics
ACL2	(VSTTE) A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
action language	(ICLP-DC) Explaining Actual Causation via Reasoning about Actions and Change (ICLP-DC) Probabalistic Action Language pBC+ (ICLP) A Probabilistic Extension of Action Language BC+
Active Objects	(AVOCS) Detecting Deadlocks in Formal System Models with Condition Synchronization
Actor	(FM) Deadlock Detection for Actor-based Coroutines
actors	(FM) SDN-Actors: Modeling and Verification of SDN Programs
Actual Cause	(ICLP-DC) Explaining Actual Causation via Reasoning about Actions and Change
ACUI	(UNIF) ACUI Unification modulo Ground Theories
Ada programming	(WPTE) Verification of Ada Programs with AdaHorn
adaptive	(VaVAS) Work-in-Progress: Adaptive Neighborhood Resizing for Stochastic Reachability in Distributed Flocking
additive monad	(LICS) Dialectica models of type theory
adequate numeral system	(ITRS)
adjoint logic	(Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
adjoint model	(Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
adjunction	(MSFP) Relating Idioms, Arrows and Monads from Monoidal Adjunctions
Adjunctions	(HDRA) Termination in linear (2,2)-categories with braidings and duals
admissibility	(SR) Beyond admissibility: Dominance between chains of strategies
admissible rules	(CL&C) Admissible tools in the kitchen of intuitionistic logic
affine term	(Linearity/TLLA) How to count linear and affine closed lambda terms?
Agda	(MSFP) Formalizing Constructive Quantifier Elimination in Agda (ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (ITP) An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory (LOLA) Experimenting with graded monads: certified grading-based program transformations (REFINE) Ordering strict partial orders to model behavioural refinement
agent policies	(ASPOCP) Towards Abstraction in ASP with an Application on Reasoning about Agent Policies
agent programming	(VaVAS) Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent
agents	(VaVAS) Social Consequence Engines (Abstract)
Aggregates	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates (ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability
aggregations in logic programming	(ICLP) Shared aggregate sets in answer set programming
AI Safety	(CAV) Safety-Aware Apprenticeship Learning
air traffic surveillance systems	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
Alarm ranking	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
Algebra	(LaSh) Declarative Dynamic Programming with Inverse Coupled Rewrite Systems
algebra in type theory	(LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
algebraic confluence	(IWC) Coherence of monoids by insertions
Algebraic crossover operators	(RCRA) Algebraic Crossover Operators for Permutations
algebraic effects	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq (LICS) Syntax and Semantics for Operations with Scopes (LICS) Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
Algebraic evolutionary computation	(RCRA) Algebraic Crossover Operators for Permutations
algebraic extensions	(SCSC) EA: New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square
Algebraic Geometry	(LICS) Polynomial Invariants for Affine Programs (Linearity/TLLA) Entropy and Complexity Lower Bounds
algebraic proof systems	(SCSC) RP: Refutation of Products of Linear Polynomials
algebraic structures	(LICS) Free Higher Groups in Homotopy Type Theory
algorithm	(CAV) Attracting Tangles to Solve Parity Games
Algorithm selection	(QBF) Portfolio-Based Algorithm Selection for Circuit QBFs
algorithm substitution attacks	(CSF) Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks
algorithmic complexity	(LICS) A modal mu perspective on solving parity games in quasipolynomial time.
algorithms	(SCSC) RP: Unknot Recognition Through Quantifier Elimination
all maximal clique partitions in a graph	(UNIF) Proximity-Based Generalization
allegories	(LICS) Allegories: decidability and graph homomorphisms
alloy	(FM) CompoSAT: Specification-Guided Coverage for Model Finding (F-IDE) Improving the Visualization of Alloy Instances
Almost Full relations	(IJCAR) Constructive Decision via Redundancy-free Proof-Search
Almost-sure winning	(CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives
alpha-equivalence	(FSCD) Fixed-Point Constraints for Nominal Equational Unification
Alternating Automata	(LICS) The State Complexity of Alternating Automata
Alternating time	(IJCAR) Focussing, MALL and the polynomial hierarchy
Alternating-time Temporal Logic	(SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions
AMBA AHB	(CAV) Strix: Explicit Reactive Synthesis Strikes Back!
anaphora	(NLCS) Paychecks, Presupposition, and Dependent Types
Android Applications	(AVOCS) Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
Android back stack	(CAV) Android Stack Systems
Android stack systems	(CAV) Android Stack Systems
Animation	(Overture) ViennaVM: a Virtual Machine for VDM-SL development (ICLP) CHRvis: Syntax and Semantics
annotation	(VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems
answer set	(ASPOCP) Syntactic Conditions for Antichain Property in Consistency Restoring Prolog
answer set computation	(ICLP) MASP-Reduce: a proposal for distributed computation of stable models
Answer Set Programming	(ICLP-DC) Scalable Robotic Intra-Logistics with Answer Set Programming (ICLP-DC) Translating P-log, LP^{MLN}, LPOD, and CR-Prolog2 into Standard Answer Set Programs (ICLP-DC) Explaining Actual Causation via Reasoning about Actions and Change (ICLP-DC) Model Revision of Logical Regulatory Networks using Logic-based Tools (ICLP-DC) Speeding Up Lazy-Grounding Answer Set Solving (LPOP) How to upgrade ASP for true dynamic modelling and solving? (LPOP) Role-Based Access Control via JASP (LPOP) Invited Talk: On the Development of Industrial Applications with ASP (ASPOCP) Towards Abstraction in ASP with an Application on Reasoning about Agent Policies (ASPOCP) selp: A Single-Shot Epistemic Logic Program Solver (ASPOCP) Invited Talk: Optimization Problems in Answer Set Programming (RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper) (RCRA) Externally Supported Models for Efficient Computation of Paracoherent Answer Sets (ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates (ICLP) First-order answer set programming as constructive proof search (ICLP) Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming (ICLP) Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP (ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming (ICLP) Exploiting Answer Set Programming with External Sources for Meta-Interpretive Learning (ICLP) Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores (ICLP) Shared aggregate sets in answer set programming (ICLP) Incremental and Iterative Learning of Answer Set Programs from Mutually Distinct Examples (ICLP) Experimenting with robotic intra-logistics domains (ICLP) Temporal Answer Set Programming on Finite Traces (ICLP) Specifying and Verbalising Answer Set Programs in Controlled Natural Language (ICLP) SMT-based Answer Set Solver CMODELS(DIFF) (System Description) (ICLP) MASP-Reduce: a proposal for distributed computation of stable models (ICLP) Introspecting Preferences In Answer Set Programming (ICLP) Learning Commonsense Knowledge through Interactive Dialogue (ICLP) Epistemic Logic Programs with World View Constraints
Answer Set Programming Extensions	(ASPOCP) A Survey of Advances in Epistemic Logic Program Solvers
Anti-unification	(FSCD) Term-Graph Anti-Unification (FSCD) Higher-Order Equational Pattern Anti-Unification (UNIF) Proximity-Based Generalization (UNIF) Towards Generalization Methods for Purely Idempotent Equational Theories (NLCS) Anti-Unification and Natural Language Processing
Apache Spark	(ICLP) MASP-Reduce: a proposal for distributed computation of stable models
Application	(ICLP) Application of Logic-Based Methods to Machine Component Design
applicative bisimulation distance	(LICS) Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
applicative first-order logic	(IJCAR) Superposition for Lambda-Free Higher-Order Logic
applicative functor	(MSFP) Relating Idioms, Arrows and Monads from Monoidal Adjunctions
applicative simulation distance	(LICS) Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
applied lambda-calculus	(LICS) Type-two polynomial-time and restricted lookahead.
Apprenticeship Learning	(CAV) Safety-Aware Apprenticeship Learning
Approximable Mappings	(Domains13) A logical view of complex analytic maps
approximate circuits	(CAV) ADAC: Automated Design of Approximate Circuits
approximate counting	(LCC) Feasibly constructive proofs of succinct weak circuit lower bounds
approximate equivalence checking	(CAV) ADAC: Automated Design of Approximate Circuits
Approximate inference	(ICLP) Constraint-Based Inference in Probabilistic Logic Programs
approximate partial order reduction	(FM) Approximate Partial Order Reduction
Approximate synthesis	(CAV) What’s hard about Boolean Functional Synthesis?
Approximation	(SMT) The next 10^4 UppSAT Approximations (IJCAR) Exploring Approximations for Floating-Point Arithmetic using UppSAT
Approximation Fixpoint Theory	(ICLP) Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs
approximation theorem	(HOR) Refining Properties of Filter Models: Sensibility, Approximability and Reducibility
architecture	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (VSTTE) Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
Arithmetic	(VSTTE) Extending VIAP to Handle Array Programs
arithmetic circuits	(LICS) Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth
Armstrong relation	(IJCAR) Automated Reasoning about Key Sets
Array	(VSTTE) Extending VIAP to Handle Array Programs
Arrays	(IJCAR) Checking Array Bounds by Abstract Interpretation and Symbolic Expressions
arrow	(MSFP) Relating Idioms, Arrows and Monads from Monoidal Adjunctions
Artificial Intelligence	(POS) MLIC: A MaxSAT-Based framework for learning interpretable classification rules (SAT) QBF as an Alternative to Courcelle's Theorem
ASMETA	(F-IDE) AsmetaF: a flattener for the ASMETA framework
ASN.1	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System
ASP	(ICLP) Translating LPOD and CR-Prolog2 into Standard Answer Set Programs
ASP systems	(LPOP) Invited Talk: On the Development of Industrial Applications with ASP
ASPIDE	(LPOP) Invited Talk: On the Development of Industrial Applications with ASP
Assertions	(ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks
Associative operad	(HDRA) Generalizations of the associative operad and convergent rewrite systems
assumptions refinement	(DS-FM) Heuristic-Based GR(1) Assumptions Refinement (FM) A Weakness Measure for GR(1) Formulae
Asynchronous	(CAV) Synthesis Of Asynchronous Reactive Programs From Temporal Specifications (ITP) An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory
Asynchronous Games	(LICS) An Asynchronous Soundness Theorem for Concurrent Separation Logic
Atom tracing	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems
atom variables	(UNIF) Rewriting with Generalized Nominal Unification
Atomic flows	(TYDI) Proof complexity of deep inference: a survey
Atomic Formula	(LaSh) Lazy Automata Techniques for WS1S
ATP	(Vampire) Testing ATP folklore: a statistical analysis of Vampire proofs. (Linearity/TLLA) Benchmarking Linear Logic Translations
Attack patterns	(GraMSec) A state machine system for insider threat detection
attack trees	(GraMSec) Deciding the Non-Emptiness of Attack trees (GraMSec) The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement (GraMSec) On Linear Logic, Functional Programming, and Attack Trees (CSF) Guided design of attack trees: a system-based approach
attacker knowledge	(CSF) Assuming you know: epistemic semantics of relational annotations for expressive flow policies
Attempto Controlled English	(ICLP) Natural Language Generation From Ontologies: Application Paper
attribute-based access control	(FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control
Authentication	(CSF) An extensive formal analysis of multi-factor authentication protocols
auto-generated code	(FM) Verifying Auto-Generated C Code from Simulink
autocorrelation	(SCSC) Hard Combinatorial Problems: A Challenge for Satisfiability
automata	(CAV) The Learnability of Symbolic Automata
automata learning	(CAV) The Learnability of Symbolic Automata (LearnAut)
Automata over infinite words	(LICS) One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
automata theory	(GS) Automata Theory and Game Semantics (LICS) The State Complexity of Alternating Automata
Automata with counters	(SR) Quantifying Bounds in Strategy Logic
Automated Algebraic Reasonings	(Coq) ComplCoq: Rewrite Hint Construction with Completion Procedures
automated complexity analysis	(LICS) Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
Automated configuration	(RCRA) On the Configuration of SAT Formulae
Automated digital control	(SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants
automated guided vehicle routing	(ICLP) Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming
automated reasoning	(CAV) Understanding and Extending Incremental Determinization for 2QBF (CAV) Model Generation for Quantified Formulas: A Taint-Based Approach (WiL) On the Combination of Resolution and SAT Procedures for Modal Theorem-Proving (IJCAR) Automated Reasoning about Key Sets (IJCAR) ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback (ITP) Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY (CSF) Alethea: A Provably Secure Random Sample Voting Protocol
automated reasonning	(SMT) Centralizing Equality Reasoning in MCSAT
automated theorem proving	(ARQNL) System Demonstration: The Higher-Order Prover Leo-III (ThEdu) Towards intuitive reasoning in axiomatic geometry (Vampire) Towards Word Sense Disambiguation by Reasoning (Vampire) Experimenting with Theory Instantiation in Vampire (Vampire) Developments in Higher-order Theorem proving within Vampire (PAAR) TFX: The TPTP Extended Typed First-order Form (IJCAR) A FOOLish Encoding of the Next State Relations of Imperative Programs (IJCAR) Efficient encodings of first-order Horn formulas in equational logic (IJCAR) ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback (IJCAR) The Higher-Order Prover Leo-III (F-IDE) Lightweight Interactive Proving inside an Automatic Program Verifier
automated trading systems	(Linearity/TLLA) Formalization of Automated Trading Systems in a Concurrent Linear Framework
Automated verification	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (CAV) Constraint-Based Synthesis of Coupling Proofs (CSF) Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (CSF) An extensive formal analysis of multi-factor authentication protocols
automatic algorithm configuration	(POS) CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances
Automatic Program Verification	(VSTTE) Extending VIAP to Handle Array Programs
Automatic Proof checking	(SCSC) RP: A Practical Polynomial Calculus for Arithmetic Circuit Verification
automatic verification	(CAV) The DEEPSEC prover (FM) Compositional Reasoning for Shared-variable Concurrent Programs (WiL) Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task?
automation	(FSCD) Completion for Logically Constrained Rewriting
Automaton State	(LaSh) Lazy Automata Techniques for WS1S
automotive	(FM) Verifying Auto-Generated C Code from Simulink
Automotive case study	(FM) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations
Autonomous	(VaVAS)
Autonomous automotive	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
Autonomous Driving	(SCSC) EA: Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving
Autonomous system	(VaVAS) Towards a verifiable decision making framework for self-driving vehicles
Autonomous vehicle	(VaVAS) Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract
autonomous vehicles	(VaVAS) Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent
avatar	(Vampire) Giving AVATAR Quantifiers to Play With
avionics systems	(FM) Model-Based Testing for Avionics Systems
Axiom Pinpointing	(IJCAR) Enumerating Justifications using Resolution
axiomatic domain theory	(Domains13) Diffeological Spaces and Semantics for Differential Programming (Domains13) Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming
Axiomatic Method	(HoTT/UF) Univalent Foundations and the Constructive View of Theories
axiomatization	(LICS) Allegories: decidability and graph homomorphisms (LICS) Riesz Modal Logic with Threshold Operators (IJCAR) Automated Reasoning about Key Sets
axioms	(IJCAR) Uniform Substitution for Differential Game Logic
B
B combinator	(FSCD) On repetitive right application of B-terms
B+ trees	(ADSL) Automating the Flow Framework
back-and-forth equivalences	(Domains13) Invited Talk: Approximating partial by total: fixpoint characterizations of back-and-forth equivalences
backdoor	(SAT) ALIAS: A Modular Tool for Finding Backdoors for SAT
backdoors	(CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF
Backtracking	(ARQNL) Pseudo-Propositional Logic (SAT) Chronological Backtracking
Backus FP	(HDRA) Minimal Bacus FP is Turing Complete
Backward exploration ·	(AVOCS) Backward reachability analysis for timed automata with data variables
backwards analysis	(ICLP) An iterative approach to precondition inference using constrained Horn clauses
Bar inductive predicates	(ITP) Proof Pearl: Constructive Extraction of Cycle Finding Algorithms
barcan formulas	(EICNCL) Proof theory for quantified monotone modal logics
Barendregt's Variable Convention	(LFMTP) Formalisation of Barendregt's Variable Convention for Generic Structures with Binders
Barrier Certificates	(CAV) Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes (FM) Vector Barrier Certificates and Comparison Systems
Basis Reduction	(ITP) A Formalization of the LLL Basis Reduction Algorithm
Bayesian inference	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
Bayesian learning	(LearnAut) Learning Tree Distributions by Hidden Markov Models
Bayesian network	(GraMSec) Combining Bayesian Networks and Fishbone Diagrams to Distinguish between Intentional Attacks and Accidental Technical Failures
BayesianInference	(VEMDP) Bayesian Verification of Chemical Reaction Networks
BDD	(RCRA) Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited
Behavioural equivalence	(CAV) The DEEPSEC prover
Behavioural metrics	(LICS) A van Benthem Theorem for Fuzzy Modal Logic
Belenios	(CSF) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios
Belief Function Theory	(PRUV) Evidential Group Decision Making Model with Belief-Based Preferences
belief merging	(PRUV) Measuring Disagreement among Knowledge Bases
Belief networks	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
benchmark	(Linearity/TLLA) Benchmarking Linear Logic Translations
Benchmarking	(LICS) A Simple and Optimal Complementation Algorithm for Büchi Automata (ICLP) Experimenting with robotic intra-logistics domains
beta reduction	(NLCS) Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus.
Beth models	(LICS) Computability Beyond Church-Turing via Choice Sequences
Betweenness Centrality	(SAT) Centrality-Based Improvements to CDCL Heuristics
Bi-directional Grammars	(ICLP) Specifying and Verbalising Answer Set Programs in Controlled Natural Language
bi-intuitionistic logic	(CL&C) Towards a Dualized Sequent Calculus with Canonicity
bicategories	(HDRA) Merge-bicategories: towards semi-strictification of higher categories
Bidding games	(SR) Infinite-Duration Richman Bidding Games
Biform theories	(ITP) HOL Light QE
BiLSTM	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Bimonad	(FSCD) Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
binarized neural network	(SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
binarized neural networks	(VSTTE) Verification of Binarized Neural Networks via Inter-Neuron Factoring
Binary Analysis	(SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
Binary Encoding	(PC) Resolution and the binary encoding of combinatorial principles
binary search tree	(ITP) Verified Analysis of Random Binary Tree Structures
binder mobility	(LFMTP) Functional programming with λ-tree syntax: a progress report
Binders	(LFMTP) Abstract Representation of Binders in OCaml using the Bindlib Library
Binding operations	(UNIF) Efficiency of a good but not linear nominal unification algorithm
Bioinformatics	(ICLP) Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic Programming
bisimulation	(VEMDP) Using Transitivity and Modularity in Chemical Reaction Network Bisimulation (LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic
bit-blasting	(SMT) Building Better Bit-Blasting for Floating-Point Problems
Bit-vectors	(CAV) BTOR2, BtorMC and Boolector 3.0
Bitcoin	(GraMSec) Tendrils of Crime: Visualizing the Diffusion of Stolen Bitcoins
Bitvectors	(WST) Complexity Analysis for Bitvector Programs
black-box optimization	(SAT) ALIAS: A Modular Tool for Finding Backdoors for SAT
BLESS	(Vampire) Towards Word Sense Disambiguation by Reasoning
Blockchain	(SMT) SMT-based Compile-time Verification of Safety Properties for Smart Contracts
blocked clauses	(IJCAR) Extended Resolution Simulates DRAT
bobs-only	(POS) Stedman and Erin Triples encoded as a SAT Problem
boolean algebra	(LICS) Classical realizability as a classifier for nondeterminism
Boolean Functional synthesis	(CAV) What’s hard about Boolean Functional Synthesis?
Boolean games	(SR) Local Equilibria in Logic-Based Multi-Player Games
Boolean polynomials	(SCSC) RP: Refutation of Products of Linear Polynomials
Boolean Satisfiability	(ICLP-DC) Model Revision of Logical Regulatory Networks using Logic-based Tools (IJCAR) A SAT-Based Approach to Learn Explainable Decision Sets (POS) Stedman and Erin Triples encoded as a SAT Problem
Boolean-valued models	(LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus
Boot code	(CAV) Model Checking Boot Code from AWS Data Centers
bottom-up	(ICLP) Top-down and Bottom-up Evaluation Procedurally Integrated
Bounded	(UNIF) Bounded ACh Unification
bounded arithmetic	(PC) Towards theories for positive polynomial time and monotone proofs with extension (PC) (PC) Complexity of expander-based reasoning and the power of monotone proofs (TYDI) Proof complexity of deep inference: a survey (LCC) Feasibly constructive proofs of succinct weak circuit lower bounds
Bounded expansion	(LICS) Parameterized circuit complexity of model-checking on sparse structures
Bounded Model Checking	(CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (CAV) Lazy Self-Composition for Security Verification
bounded model-checking	(VSTTE) Lattice-Based Refinement in Bounded Model Checking
bounded synthesis	(CAV) Synthesizing Reactive Systems from Hyperproperties (SYNT) Maximum Realizability for Linear Temporal Logic Specifications
bounds on leakage	(CSF) Symbolic Side-Channel Analysis for Probabilistic Programs
Braidings	(HDRA) Termination in linear (2,2)-categories with braidings and duals
branching programs	(PC) Branching Program Complexity of Canonical Search Problems and Proof Complexity of Formulas
broadcast communication	(CSF) A Cryptographic Look at Multi-Party Channels
Brzozowski derivatives	(LaSh) A Derivative-Based Decision Procedure for WS1S
Buchberger algorithm	(HDRA) Generalizations of the associative operad and convergent rewrite systems
Buchi Automaton	(MoRe) Logically-Constrained Reinforcement Learning
Bug Finding	(CAV) Partial Order Aware Concurrency Sampling
bug finding tool	(CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability
Bunched Implications Logic	(EICNCL) Proof Translations in BI logic
Business Process Model	(GraMSec) Disclosure Analysis of SQL Workflows
Böhm trees	(FSCD) Strict Ideal Completions of the Lambda Calculus (LICS) Probabilistic Böhm Trees and Probabilistic Separation
Büchi Automaton	(LICS) A Simple and Optimal Complementation Algorithm for Büchi Automata
C
C code	(FM) Verifying Auto-Generated C Code from Simulink
C Programming Language	(WST) Complexity Analysis for Bitvector Programs
cache coherence protocols	(CAV) Eager Abstraction for Symbolic Model Checking
Cached Address Translation	(ITP) Program Verification in the Presence of Cached Address Translation
CakeML	(VSTTE) Verified Certificate Checking for Counting Votes
calculational method	(ITP) Towards Verified Handwritten Calculational Proofs (Short Paper)
Calculational proof	(ITP) CalcCheck: a Proof Checker for Teaching the “Logical Approach to Discrete Math”
calculus of structures	(TYDI) Truely Concurrent Processes in the Calculus of Structures
call by push value	(ITP) A Formal Equational Theory for Call-by-Push-Value
call by value	(LICS) Eager Functions as Processes
call-by-name	(Linearity/TLLA) The Bang Calculus and the Two Girard's Translations
call-by-need evaluation	(WPTE) Optimizing Space of Parallel Processes
call-by-push value	(Linearity/TLLA) The Bang Calculus and the Two Girard's Translations
call-by-push-value	(Domains13) Algebra semantics of recursive computation types (LOLA) A resource modality for RAII
call-by-value	(ITRS) Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus (Linearity/TLLA) The Bang Calculus and the Two Girard's Translations
CAMUS	(SAT) Finding all Minimal Safe Inductive Sets
car assembly operations	(ICLP) Routing Driverless Transport Vehicles in Car Assembly with Answer Set Programming
Cardinality Constraint	(SAT) Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT
cardinality encodings	(SAT) PySAT: A Python Toolkit for Prototyping with SAT Oracles
Cartesian cubes	(HoTT/UF) Cubical Computational Type Theory
Cartesian Genetic Programming	(CAV) ADAC: Automated Design of Approximate Circuits
Cartesian Monoids	(HDRA) Minimal Bacus FP is Turing Complete
cartesian-closed	(Domains13) Invited Talk: Topology and Domain Theory Interfaces
Case study	(FM) Verifying Auto-Generated C Code from Simulink (RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network
Catalan numbers	(HOR) Combinatorics of explicit substitutions (extended abstract)
categorial grammar	(NLCS) Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus.
Categorical Logic	(TYDI) Some incoherent musings on deep inference and combinatorial proofs (PARIS) LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic (speaker: Pierre PRADIC) (LICS) LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic (LICS) The Syntax and Semantics of Quantitative Type Theory
Categorical model	(LICS) Syntax and Semantics for Operations with Scopes
Categorical models	(LICS) Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (HoTT/UF) Dependent Right Adjoint Types (Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
Categorical Quantum Mechanics	(FSCD) A diagrammatic axiomatisation of fermionic quantum circuits (LICS) Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics (LICS) A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics (LICS) Two complete axiomatisations of pure-state qubit quantum computing
Categorical semantics	(LICS) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (LICS) A Logical Account for Linear Partial Differential Equations (LICS) A General Framework for Relational Parametricity (HoTT/UF) Algebraic models of dependent type theory (Linearity/TLLA) Towards a Functional Language for Species of Structures
Categories of relations	(Domains13) Extending Stone Duality to Relations
categories with families	(HoTT/UF) Towards the syntax and semantics of higher dimensional type theory
Categorification	(HDRA) Termination in linear (2,2)-categories with braidings and duals
category	(LOLA) Heaps denote finitely partitioned trees
category theory	(FSCD) Call-by-name Gradual Type Theory (LICS) Dialectica models of type theory (LICS) A Generalized Modality for Recursion (LICS) What's in a game? A theory of game models (MSFP) Some No-Go Theorems for Distributive Laws (extended abstract) (SR) Compositional Game Theory
Causal Dependency	(LICS) Causal Computational Complexity of Distributed Processes
causality preservation	(CSF) A Cryptographic Look at Multi-Party Channels
Cautious Reasoning	(ICLP) Cautious Reasoning in ASP via Minimal models and Unsatisfiable Cores
ccg	(NLCS) Automated Reasoning from Polarized Parse Trees
CCSL	(REFINE) Ordering strict partial orders to model behavioural refinement
CDCL	(Isabelle) A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract) (POS) Seeking Practical CDCL Insights from Theoretical SAT Benchmarks (POS) Divide and Conquer: Towards Faster Pseudo-Boolean Solving (SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers (SAT) Chronological Backtracking (SAT) Centrality-Based Improvements to CDCL Heuristics
cdcl-cuttingplanes	(SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers
Cedille	(ITP) Efficient Mendler-Style Lambda-Encodings in Cedille
CEGIS	(CAV) Synthesis Modulo Theories
Cellular automata	(DCM) A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms
cellular cohomology	(LICS) Cellular Cohomology in Homotopy Type Theory
Centrality	(SAT) Centrality-Based Improvements to CDCL Heuristics
Certificate checking	(ITP) Tactics and Certificates in Meta Dedukti (VSTTE) Verified Certificate Checking for Counting Votes
certificates	(SAT) Polynomial-Time Validation of QCDCL Certificates
certification	(IWC) Certified Ordered Completion
certified code	(ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations
Certified execution engine	(ITP) A Coq Formalisation of SQL’S Execution Engines
certified software	(ITP) Towards Certified Meta-Programming with Typed Template-Coq
Certifying Compilation	(VSTTE) TWAM: A Certifying Abstract Machine for Logic Programs
channel composition	(FM) An Algebraic Approach for Reasoning About Information Flow
Character-level Language Model	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
chat bot	(UITP) Automated Theorem Proving in a Chat Environment
chemical computation	(VEMDP) Computing properties of stable configurations of thermodynamic binding networks
Chemical Reaction Networks	(VEMDP) Using Transitivity and Modularity in Chemical Reaction Network Bisimulation (VEMDP) Noise control for molecular computing
Chinese monoids	(HDRA) String data structures for Chinese monoids
Choice Logic	(PRUV) A new logic for jointly representing hard and soft constraints
choice sequence	(Domains13) A Brouwerian proof of the Fan Theorem
Choice sequences	(LICS) Computability Beyond Church-Turing via Choice Sequences
choiceless polynomial time	(LICS) On computability and tractability for infinite sets
Chronological Backtracking	(SAT) Chronological Backtracking
Church's type theory	(ITP) HOL Light QE
Church-Turing thesis	(WST) Objective and Subjective Specifications
circuit	(SAT) Circuit-based Search Space Pruning in QBF
Circuit complexity	(LICS) Parameterized circuit complexity of model-checking on sparse structures
circuit lower bounds	(LCC) Feasibly constructive proofs of succinct weak circuit lower bounds
circuit satisfiability	(LICS) Satisfiability in multi-valued circuits
circular proofs	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points
classical arithmetic	(LICS) A sequent calculus with dependent types for classical arithmetic
classical B	(AVOCS) Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation
classical higher-order logic	(ARQNL) System Demonstration: The Higher-Order Prover Leo-III
classical linear logic	(WiL) A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract)
classical logic	(TYDI) An introduction to deep inference (TYDI) Some incoherent musings on deep inference and combinatorial proofs (CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs
classical realizability	(LICS) A sequent calculus with dependent types for classical arithmetic (LICS) Classical realizability as a classifier for nondeterminism (ITP) Formalizing Implicative Algebras in Coq
Classical sequent calculus	(CL&C) Herbrand's Theorem as Higher-Order Recursion
Clause Learning	(ITP) A Coq Tactic for Equality Learning in Linear Arithmetic
CLF	(Linearity/TLLA) Formalization of Automated Trading Systems in a Concurrent Linear Framework
clocks	(LICS) Guarded Computational Type Theory
closed set	(Domains13) T^\omega-representations of compact sets through dyadic subbases
cluster algebra	(IWC) Complete Axiom System of Cluster Algebra
clustering	(LearnAut) Learning Several Languages from Labeled Strings: State Merging and Evolutionary Approaches
CNF	(POS) The Effect of Scrambling CNFs
CNF configuration	(RCRA) On the Configuration of SAT Formulae
Co-Simulation	(Overture) Multi-modelling of Cooperative Swarms (Overture) Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs
Coalgebra Modality	(FSCD) Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
Coarse computability	(LICS) An answer to the Gamma question
Coarse-grained modeling	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
CoCoA and MathSAT	(SCSC) EA: New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square
codatatypes	(IJCAR) Superposition with Datatypes and Codatatypes
code generation	(Isabelle) Lazy Algebraic Types in Isabelle/HOL (F-IDE) A Notebook Format for the Holistic Design of Embedded Systems (ITP) Fast Machine Words in Isabelle/HOL (ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations (ITP) Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper) (ICLP) Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP
Code Generators	(Overture) ViennaVM: a Virtual Machine for VDM-SL development
code review	(FM) Evidential and Continuous Integration of Software Verification Tools
code-generation	(Overture) Enhancing Testing of VDM-SL models
coends	(Linearity/TLLA) Proof nets, coends and the Yoneda isomorphism
Cognitive Modeling	(LPOP) Confluence Analysis of Cognitive Models with Constraint Handling Rules
cographs	(Linearity/TLLA) Coherent interaction graphs: a nondeterministic geometry of interaction for MLL
coherence	(IWC) Coherence of monoids by insertions (IWC) Coherence modulo relations (FSCD) Coherence of Gray categories via rewriting (HoTT/UF) Towards the syntax and semantics of higher dimensional type theory (HDRA) Merge-bicategories: towards semi-strictification of higher categories
coherence theorems	(LICS) Ribbon tensorial logic
coherent presentations	(HDRA) String data structures for Chinese monoids
coinduction	(FSCD) Term rewriting characterisation of LOGSPACE for finite and infinite data (PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points (PARIS) Coinductive Uniform Proofs: An Extended Abstract (speaker: Yue LI) (LICS) Every λ-Term is Meaningful for the Infinitary Relational Model (IJCAR) A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems (HCVS) Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract
coinduction up-to	(LICS) Sound up-to techniques and Complete abstract domains
Coinductive Invariants	(HCVS) Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract
coinductive types	(ITP) The Coinductive Formulation of Common Knowledge
Combination	(IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems
Combinatorial benchmarks	(SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers
combinatorial proofs	(TYDI) Some incoherent musings on deep inference and combinatorial proofs (IJCAR) From Syntactic Proofs to Combinatorial Proofs
combinatorial search algorithms	(RCRA) Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic
combinatoric	(Linearity/TLLA) How to count linear and affine closed lambda terms?
Combinatorics	(FSCD) Counting Environments and Closures (HDRA) Generalizations of the associative operad and convergent rewrite systems (Linearity/TLLA) Towards a Functional Language for Species of Structures (HOR) Combinatorics of explicit substitutions (extended abstract)
combinators	(LICS) Regular Transducer Expressions for Regular Transformations over infinite words
combinatory logic	(FSCD) On repetitive right application of B-terms (Domains13) Domain Theory for Intensional Computation
common knowledge	(ITP) The Coinductive Formulation of Common Knowledge
Common Language for Geometric Problems	(ThEdu) Rating of Geometric Automated Theorem Provers
Commonsense Reasoning	(ICLP) Learning Commonsense Knowledge through Interactive Dialogue
commutative monads	(Domains13) Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming
comonads	(Domains13) Invited Talk: Approximating partial by total: fixpoint characterizations of back-and-forth equivalences (NLCS) Propositional Attitude Operators in Homotopy Type Theory
Comparator	(CAV) Automata vs Linear-Programming Discounted-Sum Inclusion
comparator network	(POS) Competitive Sorter-based Encoding of PB-Constraints into SAT
comparison systems	(FM) Vector Barrier Certificates and Comparison Systems
CompCert	(FCS) A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler
Competition	(POS) The Effect of Scrambling CNFs
compiler	(VEMDP) Equivalence of chemical reaction networks in a CRN-to-DNA compiler framework.
compiler verification	(LOLA) A more precise, more correct stack and register model for CompCert
Compilers	(SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
complementary approximate reachability	(CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability
Complementation	(LICS) A Simple and Optimal Complementation Algorithm for Büchi Automata
complete abstract domains	(LICS) Sound up-to techniques and Complete abstract domains
complete lattices	(ITP) Formalizing Implicative Algebras in Coq
Complete Segal Spaces	(HoTT/UF) (Truncated) Simplicial Models of Type Theory
completeness	(FSCD) Completeness of Tree Automata Completion (IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (ADSL) A Complete Proof System for Basic Symbolic Heaps with Permissions
completion	(FSCD) Completion for Logically Constrained Rewriting (IJCAR) MaedMax: A Maximal Ordered Completion Tool (Coq) ComplCoq: Rewrite Hint Construction with Completion Procedures
complex analysis	(Domains13) Robust computability notions for types arising in classical analysis
Complexity	(FSCD) Counting Environments and Closures (FM) Timed Vacuity (Isabelle) Formal Verification of Bounds for the LLL Basis Reduction Algorithm (IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems (ADSL) On the Complexity of Pointer Arithmetic in Separation Logic (ADSL) The Complexity of Prenex Separation Logic with One Selector
Complexity Analysis	(LCC) A General Equational Framework for Static Profiling of Parametric Resource Usage (WST) Complexity Analysis for Bitvector Programs
complexity classes	(FSCD) Unique perfect matchings and proof nets
complexity dichotomy	(LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
Complexity measures	(SAT) Cops-Robber games and the resolution of Tseitin formulas
Complexity Proving	(WST) A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving
complexity results	(MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives
Complexity Theory	(GraMSec) Deciding the Non-Emptiness of Attack trees (Linearity/TLLA) Entropy and Complexity Lower Bounds
composition	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq (CSF) Composition Theorems for CryptoVerif and Application to TLS 1.3
compositional analysis of software systems	(AVOCS) Using SMT engine to generate Symbolic Automata
compositional model checking	(FM) To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation
compositional reasoning	(FM) Compositional Reasoning for Shared-variable Concurrent Programs
Compositional verification	(AVOCS) A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways
compositionality	(LICS) Compositional game theory (SR) Compositional Game Theory
Computability	(CAV) Program Analysis is Harder than Verification: A Computability Perspective (WiL) On Expanding Standard Notions of Constructivity (WST) Improving Static Dependency Pairs for Higher-Order Rewriting (LICS) An answer to the Gamma question (Domains13) Robust computability notions for types arising in classical analysis
computable metric space	(Domains13) T^\omega-representations of compact sets through dyadic subbases
computation and deduction	(LFMTP) Computation-as-deduction in Abella: work in progress
Computation Complexity	(LICS) Causal Computational Complexity of Distributed Processes
Computation Tree Logic	(LICS) Automaton-Based Criteria for Membership in CTL
computational complexity	(VEMDP) Using Transitivity and Modularity in Chemical Reaction Network Bisimulation (LCC) Computability over locally finite structures from algebra (LCC) Completeness in the Second Level of the Polynomial Time Hierarchy through Syntactic Properties (LICS) A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games
computational effects	(Domains13) Algebra semantics of recursive computation types
Computational Hardness	(CAV) What’s hard about Boolean Functional Synthesis?
computational model	(CSF) Composition Theorems for CryptoVerif and Application to TLS 1.3
Computational modeling	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
computational monads	(LICS) An algebraic theory of Markov processes
Computational Reductions	(ITP) Verification of PCP-Related Computational Reductions in Coq
computational soundness	(CSF) Symbolic security of garbled circuits
Computational thinking	(LICS) Sequential Relational Decomposition
computational type theory	(HoTT/UF) Cubical Computational Type Theory
computer aided security proofs	(CSF) Computer-aided proofs for multiparty computation with active security
Computer Algebra	(SCSC) RP: A Practical Polynomial Calculus for Arithmetic Circuit Verification
computer-aided cryptography	(CSF) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios
concurrency	(FM) Operational Semantics of a Weak Memory Model with Channel Synchronization (GS) Resource-Tracking Concurrent Games (LICS) ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency (VSTTE) Store Buffer Reduction in The Presence of Mixed-Size Accesses and Misalignment (LOLA) Denotational Event structure for relaxed memory (REFINE) Challenges of specifying concurrent program components
concurrency and distributed computation	(LICS) Work Analysis with Resource-Aware Session Types
Concurrency Testing	(CAV) Partial Order Aware Concurrency Sampling
Concurrent datatypes	(FM) View abstraction for systems with component identities
concurrent dictionaries	(ADSL) Automating the Flow Framework
Concurrent games	(GS) A definable game semantics for the linear quantum lambda-calculus (GS) Continuous probability distributions in concurrent games (LICS) The concurrent game semantics of Probabilistic PCF
Concurrent objects	(REFINE) Refining Santa: An Excercise in Efficient Synchronization (REFINE) Correctness of Concurrent Objects under Weak Memory Models
Concurrent operation specification	(REFINE) Challenges of specifying concurrent program components
Concurrent Process Calculi	(LICS) Causal Computational Complexity of Distributed Processes
concurrent program algebra	(FM) Encoding fairness in a synchronous concurrent program algebra
concurrent programs	(Domains13) Invited Talk: A Brief History of Denotational Semantics
Concurrent Separation Logic	(LICS) An Asynchronous Soundness Theorem for Concurrent Separation Logic (ADSL) Automating the Flow Framework
Concurrent strategies	(LICS) What's in a game? A theory of game models
Condition Synchronization	(AVOCS) Detecting Deadlocks in Formal System Models with Condition Synchronization
Conditional Independence	(CAV) Constrained Dynamic Partial Order Reduction
Conditional logic	(EICNCL) Hypersequent calculus for the logic of conditional belief: preliminary results
conditional rewriting	(IWC) Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs
conditional term rewriting	(FSCD) Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems
conditional value at risk	(LICS) Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
Confidentiality	(CSF) A Cryptographic Look at Multi-Party Channels (CSF) The Complexity of Monitoring Hyperproperties
conflict-driven clause learning	(CAV) The Proof Complexity of SMT Solvers (POS) Seeking Practical CDCL Insights from Theoretical SAT Benchmarks
conflict-driven search	(POS) Divide and Conquer: Towards Faster Pseudo-Boolean Solving (SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
confluence	(IWC) Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL (IWC) Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs (FSCD) Decreasing diagrams with two labels are complete for confluence of countable systems (FSCD) Strict Ideal Completions of the Lambda Calculus (FSCD) Confluence of Prefix-Constrained Rewrite Systems
Confluence Analysis	(LPOP) Confluence Analysis of Cognitive Models with Constraint Handling Rules
Confluence and Standardization	(HDRA) Minimal Bacus FP is Turing Complete
confluence competition	(IJCAR) Cops and CoCoWeb: Infrastructure for Confluence Tools
Confluence modulo	(IWC) Coherence modulo relations
confluence tool	(IJCAR) Cops and CoCoWeb: Infrastructure for Confluence Tools
Confusion	(LICS) Concurrency and Probability: Removing Confusion, Compositionally
Congruence	(LearnAut) Decision problems for Clark-congruential languages
Connection-based proof-search	(ARQNL) Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic
cons-free computation	(LCC) Computability over locally finite structures from algebra
Conservative approximation	(VEMDP) Conservative approximations of polymers
Conservativity	(LICS) Around Classical and Intuitionistic Linear Logics
consistency	(CAV) Monitoring Weak Consistency
Consistency Analysis	(AVOCS) Analyzing Consistency of Formal Requirements
Consistency Checking	(DS-FM) Consistency Checking of Functional Requirements
Consistency proofs	(CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs
constant-time security	(FCS) A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler
Constrained Horn Clauses	(SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses (WPTE) Verification of Ada Programs with AdaHorn (ICLP) Solving Horn Clauses on Inductive Data Types Without Induction
Constrained Optimization	(RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper)
constrained rewriting	(FSCD) Completion for Logically Constrained Rewriting (VSTTE) Loop Detection by Logically Constrained Term Rewriting (WPTE) On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems
Constraint Handling Rules	(LPOP) Confluence Analysis of Cognitive Models with Constraint Handling Rules (ICLP) Shape Neutral Analysis of Graph-based Data-structures (ICLP) CHRvis: Syntax and Semantics (ICLP) A New Proof-theoretical Linear Semantics for CHR
Constraint Handling Rules (CHR)	(LPOP) Security Policies in Constraint Handling Rules
Constraint Language	(LaSh) Automated Constraint Modelling with Conjure (LaSh) ESSENCE, A Language for Specifying Combinatorial Problems: What, Why and So What?
Constraint Logic Programming	(HCVS) Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs
Constraint Logic Programming on Finite Domains	(RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper)
Constraint Modelling	(LaSh) Automated Constraint Modelling with Conjure (LaSh) ESSENCE, A Language for Specifying Combinatorial Problems: What, Why and So What?
constraint problem	(MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives
Constraint programming	(RCRA) Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited
constraint satisfaction	(RCRA) Replaceability for constraint satisfaction problems: Algorithms, Inferences, and Complexity Patterns (RCRA) Partial (Neighbourhood) Singleton Arc Consistency for Constraint Satisfaction Problems
Constraint Satisfaction Problem	(LICS) Satisfiability in multi-valued circuits (IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems
constraint satisfaction problems	(LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
Constraint satisfaction processing	(ICLP) SMT-based Answer Set Solver CMODELS(DIFF) (System Description)
Constraint Solving	(SCSC) EA: Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving (LaSh) Automated Constraint Modelling with Conjure (IJCAR) A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems (HCVS) Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions (ICLP) Application of Logic-Based Methods to Machine Component Design
Constraint Systems	(SCSC) EA: Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving
Constraint-based synthesis	(CAV) Constraint-Based Synthesis of Coupling Proofs
Constraint-based verification	(CAV) Constraint-Based Synthesis of Coupling Proofs
constraints	(LPOP) Easier Rules and Constraints for Programming (WiL) Towards a Logical Framework for Latent Variable Modelling (PRUV) Evidential Group Decision Making Model with Belief-Based Preferences (ICLP) Constraint-Based Inference in Probabilistic Logic Programs (ICLP) Constraint Answer Set Programming without Grounding (ICLP) Epistemic Logic Programs with World View Constraints
constraints solver	(POS) Competitive Sorter-based Encoding of PB-Constraints into SAT
constructive	(MSFP) Formalizing Constructive Quantifier Elimination in Agda
Constructive Decidability	(IJCAR) Constructive Decision via Redundancy-free Proof-Search
constructive mathematics	(LICS) Computable decision making on the reals and other spaces via partiality and nondeterminism
Constructive Type Theory	(LFMTP) Formalization in Constructive Type Theory of the Standardization Theorem
Constructive View of Theories	(HoTT/UF) Univalent Foundations and the Constructive View of Theories
constructivism	(WiL) Towards a Logical Framework for Latent Variable Modelling
contact logics	(UNIF) About the unification type of topological logics over Euclidean spaces
context-free	(TERMGRAPH) A framework for rewriting families of string diagrams
Context-free Grammars	(ITP) Verification of PCP-Related Computational Reductions in Coq (LearnAut) Decision problems for Clark-congruential languages
contextual equivalence	(GS) Automata Theory and Game Semantics (ITP) A Formal Equational Theory for Call-by-Push-Value (WPTE) Automating the Diagram Method to Prove Correctness of Program Transformations
contextual fibrancy	(HoTT/UF) Robust Notions of Contextual Fibrancy
contextuality	(LICS) Logical paradoxes in quantum computation
Continuation Semantics	(Domains13) Abstractness of Continuation Semantics for Asynchronous Concurrency
Continuous computation	(CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs
Continuous delivery	(Overture) Integrating VDM-SL into the continuous delivery pipelines of cloud-based software
continuous systems	(FM) Vector Barrier Certificates and Comparison Systems
continuous validation	(Overture) Enhancing Testing of VDM-SL models
continuous valuation	(Domains13)
Continuous-time Markov chain	(CAV) Monitoring CTMCs By Multi-Clock Timed Automata
contract-based verification	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
contractibility	(FSCD) Proof nets for bi-intuitionistic linear logic
Contraction	(TYDI) Proof complexity of deep inference: a survey
control	(VaVAS) Work-in-Progress: Adaptive Neighborhood Resizing for Stochastic Reachability in Distributed Flocking
control flow	(MLP) Deep Learning On Code with an Unbounded Vocabulary
control improvisation	(CAV) Reactive Control Improvisation
Control parameters	(ITP) Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY
Control-Flow Refinment	(WST) Control-Flow Refinement via Partial Evaluation
Controlled Natural Language	(ICLP-DC) Knowledge Authoring and Question Answering via Controlled Natural Language (UITP) Text-Orientated Formal Mathematics (ICLP) Natural Language Generation From Ontologies: Application Paper
Controlled Natural Languages	(ICLP) Specifying and Verbalising Answer Set Programs in Controlled Natural Language
controller synthesis	(DS-FM) Heuristic-Based GR(1) Assumptions Refinement (CAV) Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty
controller system	(MoRe) Comfort and Energy Optimization for Floor Heating Systems
conversion algorithm	(CAV) A Direct Encoding for NNC Polyhedra
convex polyhedra	(CAV) A Direct Encoding for NNC Polyhedra
Cooperative Scheduling	(FM) Deadlock Detection for Actor-based Coroutines
Coq	(FSCD) Cumulative Inductive Types in Coq (LFMTP) Sharing a library between proof assistants: reaching out to the HOL family (FM) Modular Verification of Programs with Effects and Effect Handlers in Coq (AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base (Coq) Towards a formalization of the guard condition (Coq) Classical Analysis with Coq (Coq) Procrastination, A proof engineering technique (Coq) Teaching Your Rooster to Crow in C (ITP) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs (ITP) Formalizing Implicative Algebras in Coq (ITP) Towards Certified Meta-Programming with Typed Template-Coq (ITP) A Coq Formalisation of SQL’S Execution Engines (ITP) Reification by Parametricity (VSTTE) A Java bytecode formalisation (LOLA) Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic
Coq library	(Coq) Preliminary Report on the Yalla Library
Coq proof assistant	(FCS) A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler
Core SAT	(SAT) Chronological Backtracking
Corecursion	(HCVS) Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract
correctness	(REFINE) Correctness of Concurrent Objects under Weak Memory Models (WPTE) Automating the Diagram Method to Prove Correctness of Program Transformations
Correctness by extraction	(ITP) Proof Pearl: Constructive Extraction of Cycle Finding Algorithms
correctness criteria	(FSCD) Unique perfect matchings and proof nets (Linearity/TLLA) Coherent interaction graphs: a nondeterministic geometry of interaction for MLL
Correctness Enhancement	(REFINE) Programming Without Refinement
Correctness proof	(HCVS) A simple functional presentation and an inductive correctness proof of the Horn algorithm
Correctness proofs	(VSTTE) Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications
Correspondence theory	(LICS) A van Benthem Theorem for Fuzzy Modal Logic
Cost Analysis	(WST) Inference of Linear Upper-Bounds on the Expected Cost by Solving Cost Relations (WST) Control-Flow Refinement via Partial Evaluation
Cost bounded reachability	(MoRe) Multiple Objectives and Cost Bounds in MDP
Cost relations	(WST) Inference of Linear Upper-Bounds on the Expected Cost by Solving Cost Relations
counter-example	(FM) Producing Explanations for Rich Logics
CounterExample Guided Inductive Synthesis	(SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants
Counterexample-guided Algorithms	(SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
Counterexample-Guided Inductive Synthesis	(CAV) Safety-Aware Apprenticeship Learning
counterexamples	(ARQNL) Evidence Extraction from Parameterised Boolean Equation Systems (VSTTE) Executable Counterexamples in Software Model Checking
countermodel construction	(EICNCL) A Forward Calculus for Countermodel Construction in IPL
counting classes	(LICS) Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth
Courcelle's Theorem	(LaSh) Courcelle’s Theorem – A Game-Theoretic Approach
Covering Theory	(HoTT/UF) Cohesive Covering Theory
CPS translation	(Linearity/TLLA) From Linear Logic to Cyclic Sharing
CR-Prolog	(ICLP-DC) Translating P-log, LP^{MLN}, LPOD, and CR-Prolog2 into Standard Answer Set Programs
CR-Prolog2	(ICLP) Translating LPOD and CR-Prolog2 into Standard Answer Set Programs
Crafted benchmarks	(POS) Seeking Practical CDCL Insights from Theoretical SAT Benchmarks (SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers
Craig Interpolation	(IJCAR) Efficient Interpolation for the Theory of Arrays
Crime tracing	(GraMSec) Tendrils of Crime: Visualizing the Diffusion of Stolen Bitcoins
critical complexity region	(RCRA) Replaceability for constraint satisfaction problems: Algorithms, Inferences, and Complexity Patterns
critical pair	(FSCD) Confluence of Prefix-Constrained Rewrite Systems
critical software assurance	(AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
Critical Systems	(AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks
CRN	(VEMDP) Bayesian Verification of Chemical Reaction Networks
CRN equivalence	(VEMDP) Equivalence of chemical reaction networks in a CRN-to-DNA compiler framework.
cross-fertilization	(LICS) Sound up-to techniques and Complete abstract domains
cross-section property	(HDRA) String data structures for Chinese monoids
crowds	(FM) An Algebraic Approach for Reasoning About Information Flow
cryptographic CNF instances	(POS) CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances
cryptographic constant-time	(CSF) Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time”
Cryptographic protocol	(CAV) The DEEPSEC prover
Cryptographic protocols	(FCS) Homomorphisms and Minimality for Enrich-by-Need Security Analysis
cryptographic schemes	(CSF) Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks
Cryptographic software	(CAV) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks
Cryptography	(CAV) Continuous formal verification of Amazon s2n
CSP	(IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems
CSP Solver	(LPOP) A Picat-based XCSP Solver - from Parsing, Modeling, to SAT Encoding
cubical sets	(FSCD) Internal Universes in Models of Homotopy Type Theory (HoTT/UF) The definitional symmetric cubical structure of types in type theory with equality defined by abstraction over an interval (HoTT/UF) Ordered Cubes
cubical type theory	(LICS) On Higher Inductive Types in Cubical Type Theory (LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (HoTT/UF) The definitional symmetric cubical structure of types in type theory with equality defined by abstraction over an interval (HoTT/UF) Cubical Computational Type Theory (HoTT/UF) Cubical Assemblies and the Independence of the Propositional Resizing Axiom (HoTT/UF) Dependent Right Adjoint Types
Curry-Howard	(LICS) Classical realizability as a classifier for nondeterminism (CL&C) On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains
Curry-Howard correspondence	(WiL) A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract) (SAT) Local Soundness for QBF Calculi
Curry-Howard isomorphism	(RCRA) Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic
cut elimination	(ITRS) Intersection Subtyping with Constructors (LICS) Unification nets: canonical proof net quantifiers
cut-elimination	(CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs (CL&C) Fast cut-elimination using proof terms: an empirical study
Cut-elimination theorem	(EICNCL) Sequent Calculi for Logic that Includes an Infinite Number of Modalities
Cutting and Packing	(RCRA) An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
cutting planes	(PC) Branching Program Complexity of Canonical Search Problems and Proof Complexity of Formulas (POS) Divide and Conquer: Towards Faster Pseudo-Boolean Solving (SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
Cyber Security	(PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication
Cyber-Physical system	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (FM) Towards `Verifying' a Water Treatment System
cyber-physical systems	(FM) Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning (LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
Cybercrime	(GraMSec) Tendrils of Crime: Visualizing the Diffusion of Stolen Bitcoins
Cycle finding	(ITP) Proof Pearl: Constructive Extraction of Cycle Finding Algorithms
Cyclic graphs	(TERMGRAPH) Drags: an algebraic framework for graph rewriting
cyclic induction	(CL&C) Validating Back-links of FOL-ID Cyclic Pre-proofs
cyclic lambda calculus	(Linearity/TLLA) From Linear Logic to Cyclic Sharing
cyclic proof	(ADSL) Cyclic Theorem Prover for Separation Logic by Magic Wand
Cyclic proofs	(PARIS) Transitive Closure Logic: Infinitary and Cyclic Proof Systems (PARIS) On the Logical Complexity of Cyclic Arithmetic (AVOCS) An Entailment Checker for Separation Logic with Inductive Definitions (ADSL) Labelled Cyclic Proofs for Separation Logic (CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs
cyclic sharing	(Linearity/TLLA) From Linear Logic to Cyclic Sharing
Cyclic term-graps	(FSCD) Term-Graph Anti-Unification
Cylindrical Algebraic Decomposition	(SCSC) RP: Towards Incremental Cylindrical Algebraic Decomposition in Maple (SCSC) RP: Evaluation of Equational Constraints for CAD in SMT Solving
D
D-optimaldesigns	(SCSC) Hard Combinatorial Problems: A Challenge for Satisfiability
Daniell-Kolmogorov theorem	(Domains13)
data compression	(IWC) Complete Axiom System of Cluster Algebra
Data Driven modelling	(VEMDP) Bayesian Verification of Chemical Reaction Networks
data flow	(VSTTE) A Tree-Based Approach to Data Flow Proofs
Data Races	(LICS) An Asynchronous Soundness Theorem for Concurrent Separation Logic
Data words	(LICS) Logics for Word Transductions with Synthesis (LICS) Playing with Repetitions in Data Words Using Energy Games
Data-structures	(ICLP) Shape Neutral Analysis of Graph-based Data-structures
database theory	(LICS) Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable.
Databases	(ITP) A Coq Formalisation of SQL’S Execution Engines
Datalog	(LPOP) Security Policies in Constraint Handling Rules (ASPOCP) Datalog for Static Analysis Involving Logical Formulae (IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description (ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability
datatypes	(IJCAR) Datatypes with Shared Selectors (IJCAR) Superposition with Datatypes and Codatatypes (ITP) Boosting the Reuse of Formal Specifications (ITP) Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes
de Groot duality	(Domains13) Applications of entailments: de Groot duality
Deadlock	(FM) A lightweight deadlock analysis technique of object-oriented programs
Deadlock Analysis	(AVOCS) Detecting Deadlocks in Formal System Models with Condition Synchronization
Deadlock Detection	(FM) Deadlock Detection for Actor-based Coroutines (FM) Dynamic Symbolic Verification of MPI Programs
deadlock-freedom	(WiL) A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract)
Decentralized planning	(FM) Multi-Robot LTL Planning Under Uncertainty
Decidability	(FM) The Compound Interest in Relaxing Punctuality (SYNT) On the Expressiveness of HyperLTL Synthesis (LICS) Allegories: decidability and graph homomorphisms (ADSL) The Complexity of Prenex Separation Logic with One Selector (MSFP) Formalizing Constructive Quantifier Elimination in Agda (LearnAut) Decision problems for Clark-congruential languages
decision	(IJCAR) FORT 2.0
Decision making	(VaVAS) Towards a verifiable decision making framework for self-driving vehicles
Decision Model and Notation (DMN)	(LPOP) Logic-based Methods for Software Engineers and Business People
Decision Modeling	(LPOP) Logic-based Methods for Software Engineers and Business People
Decision Modelling	(ICLP) Application of Logic-Based Methods to Machine Component Design
decision procedure	(CAV) Android Stack Systems (LaSh) Lazy Automata Techniques for WS1S (LaSh) A Derivative-Based Decision Procedure for WS1S (IJCAR) A Separation Logic with Data: Small Models and Automation (IJCAR) Deciding the First-Order Theory of an Algebra of Feature Trees with Updates (IJCAR) Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic (ADSL) Sloth: Separation Logic and Theories via Small Models
Decision Procedures	(SCSC) EA: Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT (LaSh) Decidable Linear Tree Constraints (IJCAR) Datatypes with Shared Selectors (IJCAR) A Why3 framework for reflection proofs and its application to GMP's algorithms
decisiveness	(MoRe) Stochastic o-minimal hybrid systems
Declarative Algorithms	(RCRA) Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic (ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability
declarative programming	(LPOP) A software system should be declarative except where it interacts with the real world (FM) Variant Analysis with QL (PRUV) A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems
Declarative Prover	(ThEdu) Students' Proof Assistant (SPA)
declassification	(CSF) Assuming you know: epistemic semantics of relational annotations for expressive flow policies
decoupled approach	(CAV) Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics
decreasing diagrams	(FSCD) Decreasing diagrams with two labels are complete for confluence of countable systems
deduction	(WPTE) Automating the Diagram Method to Prove Correctness of Program Transformations
Deductive interactive program verification	(UITP) Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons Learned
Deductive program verification	(IJCAR) A Why3 framework for reflection proofs and its application to GMP's algorithms
Deductive programs verification	(SMT) Alt-Ergo 2.2
deductive verification	(CAV) Eager Abstraction for Symbolic Model Checking (F-IDE) Experience Report on Formally Verifying Parts of OpenJDK's API with KeY (F-IDE) Lightweight Interactive Proving inside an Automatic Program Verifier (ITP) Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY (VSTTE) Practical Methods for Reasoning about Java 8's Functional Programming Features
Dedukti	(LFMTP) Sharing a library between proof assistants: reaching out to the HOL family (ITP) Tactics and Certificates in Meta Dedukti
Deduplication	(PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication
deep embedding	(Coq) Preliminary Report on the Yalla Library
deep inference	(TYDI) Deep-Inference Intersection Types (TYDI) Proof complexity of deep inference: a survey (TYDI) Deep Inference, Herbrand's Theorem and Expansion Proofs (TYDI) Truely Concurrent Processes in the Calculus of Structures (TYDI) An introduction to deep inference (TYDI) Some incoherent musings on deep inference and combinatorial proofs
Deep Learning	(MLP) Deep Learning On Code with an Unbounded Vocabulary (MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Deficiency	(SAT) Minimal unsatisfiability and minimal strongly connected digraphs
definability	(LICS) Definable decompositions for graphs of bounded linear cliquewidth
Definable	(GS) A definable game semantics for the linear quantum lambda-calculus
definable while programs	(LICS) On computability and tractability for infinite sets
delay differential equations	(CAV) Inner and Outer Approximating Flowpipes for Delay Differential Equations
Delta-completeness	(CAV) Delta-Decision Procedures for Exists-Forall Problems over the Reals
denotation	(LICS) Every λ-Term is Meaningful for the Infinitary Relational Model
denotational model	(Linearity/TLLA) A semantic conjecture on second-order MLL and its complexity consequences (work in progress)
denotational semantics	(FSCD) Call-by-name Gradual Type Theory (FSCD) The clocks they are adjunctions. Denotational semantics for Clocked Type Theory (PARIS) What makes guarded types tick? (Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (LICS) Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (LICS) Probabilistic stable functions on discrete cones are power series. (LICS) Boolean-Valued Semantics for Stochastic Lambda-Calculus (Domains13) Algebra semantics of recursive computation types (Domains13) Invited Talk: A Brief History of Denotational Semantics (Linearity/TLLA) The Bang Calculus and the Two Girard's Translations (CL&C) A Denotational Model of the Typed Lambda-Mu Calculus (HOR) The next 700 (type-theoretical) denotational models ? (HOR) Refining Properties of Filter Models: Sensibility, Approximability and Reducibility (LOLA) Heaps denote finitely partitioned trees (LOLA) Denotational Event structure for relaxed memory
deontic logis	(ARQNL) System Demonstration: The Higher-Order Prover Leo-III
Dependant Types	(WST) Termination of Lambda-Pi modulo rewriting using the size-change principle
dependence maps	(SR) Dependences in Strategy Logic
Dependency	(AVOCS) Detecting Deadlocks in Formal System Models with Condition Synchronization
dependency graph	(ASPOCP) Syntactic Conditions for Antichain Property in Consistency Restoring Prolog
dependent choice	(LICS) A sequent calculus with dependent types for classical arithmetic
dependent product types	(LICS) Dialectica models of type theory
Dependent Refinement Types	(CAV) Propositional Dynamic Logic for Higher-Order Functional Programs (LICS) A Fixpoint Logic and Dependent Effects for Temporal Property Verification
dependent temporal effects	(LICS) A Fixpoint Logic and Dependent Effects for Temporal Property Verification
dependent type theory	(FSCD) Internal Universes in Models of Homotopy Type Theory (LICS) Dialectica models of type theory (NLCS) Paychecks, Presupposition, and Dependent Types (HoTT/UF) Algebraic models of dependent type theory
dependent types	(ICLP-DC) Proof-relevant resolution for elaboration of programming languages (LICS) Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (LICS) A sequent calculus with dependent types for classical arithmetic (LICS) Guarded Computational Type Theory (ITP) Tactics and Certificates in Meta Dedukti (ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (Linearity/TLLA) Substructural Calculi with Dependent Types (ICLP) Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
dependently typed programming	(MSFP) Everybody's Got To Be Somewhere (ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware
derivational complexity	(WST) Embracing Infinity - Termination of String Rewriting by Almost Linear Weight Functions
derivationism	(WiL) Can every real proof be represented by a formal proof? The Hilbert-Gentzen thesis
Deriving Reliable Programs	(REFINE) Programming Without Refinement
Description logic	(LICS) A van Benthem Theorem for Fuzzy Modal Logic (IJCAR) Enumerating Justifications using Resolution
description logics	(IJCAR) FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics (PRUV) Reasoning about exceptions in ontologies: from the lexicographic closure to the skeptical closure (FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control
descriptive complexity	(LCC) Completeness in the Second Level of the Polynomial Time Hierarchy through Syntactic Properties (LICS) Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth (LICS) A modal mu perspective on solving parity games in quasipolynomial time.
design automation	(CAV) ADAC: Automated Design of Approximate Circuits
design by contract	(F-IDE) Experience Report on Formally Verifying Parts of OpenJDK's API with KeY (ITP) Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY
Design Space Exploration	(Overture) Design Space Exploration for Secure Building Control
destructors	(LOLA) A resource modality for RAII
determinacy	(LICS) Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable.
Deterministic Automata	(CAV) Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (LICS) One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
Deterministic Parity Automaton	(CAV) Strix: Explicit Reactive Synthesis Strikes Back!
DFA	(WiL) First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation
Diagrammatic Reasoning	(LICS) Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics (LICS) A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics
dialectica category	(Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
Dialectica interpretation	(LICS) Dialectica models of type theory
diamond lemma	(IWC) The diamond lemma for free modules
diffeological spaces	(Domains13) Diffeological Spaces and Semantics for Differential Programming
differential dynamic logic	(LICS) Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
differential equation axiomatization	(LICS) Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
Differential Equations	(VEMDP) Conservative approximations of polymers (LICS) A Logical Account for Linear Partial Differential Equations
differential game logic	(IJCAR) Uniform Substitution for Differential Game Logic
differential ghosts	(LICS) Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
Differential Linear Logic	(LICS) A Logical Account for Linear Partial Differential Equations (Linearity/TLLA) Models of Linear Logic based on the Schwartz epsilon product (Linearity/TLLA) Towards a Functional Language for Species of Structures
differential programming	(Domains13) Diffeological Spaces and Semantics for Differential Programming
Digital libraries	(LICS) Computability Beyond Church-Turing via Choice Sequences
Diller-Nahm variant	(LICS) Dialectica models of type theory
Diophantine equations	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
direct-manipulation interaction	(UITP) Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons Learned
directed complete	(Domains13) Invited Talk: Topology and Domain Theory Interfaces
Discounted-sum determinization	(CAV) Automata vs Linear-Programming Discounted-Sum Inclusion
Discounted-sum inclusion	(CAV) Automata vs Linear-Programming Discounted-Sum Inclusion
discrete polymorphism	(ITRS) Gradual Intersection Types
Discrete-Event	(Overture) Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs
discrete-time linear system	(CAV) Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics
Display calculi	(EICNCL) Effective Translations between Display and Labelled Proofs for Tense Logics
display map category	(LICS) Dialectica models of type theory
distance bounding protocols	(FCS) Proving physical proximity using symbolic models
Distance fraud	(FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols
Distance-bounding protocols	(FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols
distribute consensus protocols	(CAV) Eager Abstraction for Symbolic Model Checking
distributed autonomous systems	(VaVAS) Towards a Hierarchical-Control Architecture for Distributed Autonomous Systems (Extended Abstract - Paper)
distributed computing	(CAV) Peregrine: A Tool for the Analysis of Population Protocols
distributed concurrent systems	(FM) SDN-Actors: Modeling and Verification of SDN Programs
Distributed Protocols	(HCVS) Declarative Parameterized Verification of Topology-sensitive Distributed Protocols
distributed systems	(FM) Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE (ICLP) MASP-Reduce: a proposal for distributed computation of stable models
Distribution based objectives	(LICS) Distribution-based objectives for Markov Decision Processes
distributive laws	(MSFP) Some No-Go Theorems for Distributive Laws (extended abstract)
division	(POS) Divide and Conquer: Towards Faster Pseudo-Boolean Solving
DLVSYSTEM srl	(LPOP) Invited Talk: On the Development of Industrial Applications with ASP
DMN	(ICLP) Application of Logic-Based Methods to Machine Component Design
DNA algorithmic self-assembly	(VEMDP) Computational Approaches for the Programmed Assembly of Nanocellulose Meshes
DNF	(LearnAut) Toward Learning Boolean Functions from Positive Examples
Dolev-Yao Attacker	(CAV) Model checking indistinguishability of randomized security protocols
domain	(Domains13)
domain equation	(Domains13) Algebra semantics of recursive computation types
domain specific languages	(ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware
domain theory	(Domains13) Domain Theory for Intensional Computation (Domains13) Invited Talk: A Brief History of Denotational Semantics (Domains13) Invited Talk: Topology and Domain Theory Interfaces
domain-level strand displacement	(VEMDP) Equivalence of chemical reaction networks in a CRN-to-DNA compiler framework.
domain-specific formal languages	(F-IDE) Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents
Domain-specific languages	(CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
dominance	(SR) Beyond admissibility: Dominance between chains of strategies
Double Description method	(CAV) A Direct Encoding for NNC Polyhedra
Double negation	(LICS) Around Classical and Intuitionistic Linear Logics
Double-pushout graph transformation	(TERMGRAPH) Semantics-Preserving DPO-Based Term Graph Rewriting
Double-pushout rewriting	(LICS) Rewriting with Frobenius
downward closures	(LICS) Separability by piecewise testable languages and downward closures beyond subwords
DPRM Theorem	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
drat	(IJCAR) Extended Resolution Simulates DRAT
DRAT proofs	(POS) Two flavors of DRAT
DSL	(Coq) Teaching Your Rooster to Crow in C
dual-rail encoding	(PC) On Dual-Rail Based MaxSAT Solving
duality	(LICS) Riesz Modal Logic with Threshold Operators
dualized proof system	(CL&C) Towards a Dualized Sequent Calculus with Canonicity
Dynamic analysis	(CAV) Quasi-Optimal Partial Order Reduction
Dynamic applications	(ICLP) Experimenting with robotic intra-logistics domains
Dynamic data structures	(CAV) Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs
Dynamic domains	(LPOP) How to upgrade ASP for true dynamic modelling and solving?
dynamic epistemic logic	(ITP) Software Tool Support for Modular Reasoning in Modal Logics of Actions
Dynamic language	(CAV) Nagini: A Static Verifier for Python
Dynamic Languages	(CAV) MaxSMT-Based Type Inference for Python 3
Dynamic Logic	(FM) The Compound Interest in Relaxing Punctuality (LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
Dynamic nets	(LICS) Concurrency and Probability: Removing Confusion, Compositionally
Dynamic Partial Order Reduction	(CAV) Constrained Dynamic Partial Order Reduction
Dynamic Programming	(LaSh) Solving #SAT by Parameterized Algorithms: Exploiting Small Treewidth (LaSh) Declarative Dynamic Programming with Inverse Coupled Rewrite Systems (MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network (ITP) Verified Memoization and Dynamic Programming
Dynamic Verification	(FM) Dynamic Symbolic Verification of MPI Programs
Dynamical Systems	(Linearity/TLLA) Entropy and Complexity Lower Bounds
E
e-voting	(CSF) Alethea: A Provably Secure Random Sample Voting Protocol
EasyCrypt	(CSF) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios (CSF) Computer-aided proofs for multiparty computation with active security (CSF) Formal Security Proof of CMAC and its Variants
Eckmann-Hilton morphism	(HDRA) Towards a fully formalized definition of syllepsis in weak higher categories
Economic Reasoning	(SCSC) RP: Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics
Economics	(ITP) Towards Formal Foundations for Game Theory (Short Paper)
effectful bisimilarity	(LICS) Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
Effective translations	(EICNCL) Effective Translations between Display and Labelled Proofs for Tense Logics
Efficiency	(UNIF) Efficiency of a good but not linear nominal unification algorithm
Efficient Attractor	(PLR) An Efficient Zielonka's Algorithm for Parallel Parity Games
efficient computation	(ICLP) Shared aggregate sets in answer set programming
Egraph	(SMT) Centralizing Equality Reasoning in MCSAT
Eilenberg-Moore Category	(FSCD) Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
elaboration	(ICLP-DC) Proof-relevant resolution for elaboration of programming languages
Eldarica	(WPTE) Verification of Ada Programs with AdaHorn
Electronic Voting	(CAV) Model checking indistinguishability of randomized security protocols
elementary linear logic	(Linearity/TLLA) A semantic conjecture on second-order MLL and its complexity consequences (work in progress)
elementary semantics	(SR) Dependences in Strategy Logic
ellipsoid method	(LICS) Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
embedded domain specific language	(GraMSec) On Linear Logic, Functional Programming, and Attack Trees
Embedded systems	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
Empirical evaluation	(CAV) Automata vs Linear-Programming Discounted-Sum Inclusion
EMVCo	(Overture) VDM at large: analysing the EMV Next Generation Kernel
energy games	(LICS) Playing with Repetitions in Data Words Using Energy Games
energy-efficient computing	(CAV) ADAC: Automated Design of Approximate Circuits
engineering mathematics	(ThEdu) Lucas Interpretation from Programmers’ Perspective
enriched categories	(Domains13) Higher-dimensional categories: recursion on extensivity
enriched category theory	(LICS) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
entailment check	(ADSL) Cyclic Theorem Prover for Separation Logic by Magic Wand
entailment relation	(Domains13) Applications of entailments: de Groot duality
Entitity Resolution	(PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication
epistemic logic	(FM) Timed Epistemic Knowledge Bases for Social Networks (ITP) The Coinductive Formulation of Common Knowledge (EICNCL) Hypersequent calculus for the logic of conditional belief: preliminary results
Epistemic Logic Program Solvers	(ASPOCP) A Survey of Advances in Epistemic Logic Program Solvers
Epistemic Logic Programs	(ASPOCP) selp: A Single-Shot Epistemic Logic Program Solver (ASPOCP) A Survey of Advances in Epistemic Logic Program Solvers (ICLP) Epistemic Logic Programs with World View Constraints
Epistemic Negations	(ASPOCP) A Survey of Advances in Epistemic Logic Program Solvers
epistemic specification	(ICLP) Introspecting Preferences In Answer Set Programming
Epistemic Specifications	(ASPOCP) A Survey of Advances in Epistemic Logic Program Solvers (ICLP) Epistemic Logic Programs with World View Constraints
equality by abstraction over an interval	(HoTT/UF) The definitional symmetric cubical structure of types in type theory with equality defined by abstraction over an interval
equational constraints	(SCSC) RP: Evaluation of Equational Constraints for CAD in SMT Solving
equational logic	(LICS) An algebraic theory of Markov processes (IJCAR) Efficient encodings of first-order Horn formulas in equational logic
equational rewriting	(UNIF) Knowledge Problems in Equational Extensions of Subterm Convergent Theories
Equational theories	(PC) Towards theories for positive polynomial time and monotone proofs with extension (FSCD) Fixed-Point Constraints for Nominal Equational Unification (FSCD) Higher-Order Equational Pattern Anti-Unification (UNIF) Towards Generalization Methods for Purely Idempotent Equational Theories
equational theory	(UNIF) Unification based on generalized embedding (ITP) A Formal Equational Theory for Call-by-Push-Value (LOLA) A graph-rewriting perspective of the beta-law
Equilibrium Logic	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates
Equivalence	(LearnAut) Decision problems for Clark-congruential languages (FCS) A Homotopical Approach to Cryptography
equivalence relations	(LICS) Unary negation fragment with equivalence relations has the finite model property
erasure	(LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
Erin	(POS) Stedman and Erin Triples encoded as a SAT Problem
Erin Triples	(POS) Stedman and Erin Triples encoded as a SAT Problem
Erlang	(HCVS) Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs
essential unification	(UNIF) Unification based on generalized embedding
essentially algebraic theories	(Domains13) Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming
Ethereum	(SMT) SMT-based Compile-time Verification of Safety Properties for Smart Contracts (CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (VSTTE) Towards verification of Ethereum smart contracts: a formalization of core of Solidity
Evaluable Functions	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates
Evaluation	(POS) Seeking Practical CDCL Insights from Theoretical SAT Benchmarks (POS) The Effect of Scrambling CNFs
Event Calculus	(ICLP) Learning Commonsense Knowledge through Interactive Dialogue
Event structures	(GS) Continuous probability distributions in concurrent games (LICS) Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (LICS) The concurrent game semantics of Probabilistic PCF (LOLA) Denotational Event structure for relaxed memory
evidential verification	(FM) Evidential and Continuous Integration of Software Verification Tools
Evolution systems	(VEMDP) Conservative approximations of polymers
exceptions	(LOLA) A resource modality for RAII
exchange	(Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
exchange rule	(Coq) Preliminary Report on the Yalla Library
Executable Harnesses	(VSTTE) Executable Counterexamples in Software Model Checking
Executable Specifications	(ICLP) Specifying and Verbalising Answer Set Programs in Controlled Natural Language
execution time	(ITRS) Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus
exhaustive and randomized data generation	(LFMTP) Property-Based Testing of Abstract Machines: an Experience Report
Existential Rules	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description (PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication
expander graphs	(PC) Complexity of expander-based reasoning and the power of monotone proofs
expansion proofs	(TYDI) Deep Inference, Herbrand's Theorem and Expansion Proofs (CL&C) Fast cut-elimination using proof terms: an empirical study
expected shortfall	(LICS) Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
Expected Utility	(ITP) Towards Formal Foundations for Game Theory (Short Paper)
experimental analysis	(SAT) Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
Experiments	(POS) A Problem Meta-Data Library for Research in SAT (ICLP) Improving Candidate Quality of Probabilistic Logic Models
Expert Systems	(ICLP) Application of Logic-Based Methods to Machine Component Design
explainable decision set	(IJCAR) A SAT-Based Approach to Learn Explainable Decision Sets
explanation	(ICLP-DC) Explaining Actual Causation via Reasoning about Actions and Change (FM) Producing Explanations for Rich Logics
explanatory analysis	(FM) To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation
explicit induction reasoning	(PARIS) Useless Explicit Induction Reasoning
explicit substitution	(HOR) Combinatorics of explicit substitutions (extended abstract)
Exposed Datapath Architectures	(ICLP) Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP
expressiveness	(LICS) A Theory of Register Monitors
extended resolution	(IJCAR) Extended Resolution Simulates DRAT
Extension	(NLCS) Propositional Attitude Operators in Homotopy Type Theory
extensive categories	(Domains13) Higher-dimensional categories: recursion on extensivity
extensive category	(LICS) Dialectica models of type theory
extensive-form games	(GraMSec) The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement
External calculi	(EICNCL) Effective Translations between Display and Labelled Proofs for Tense Logics
extraction	(Coq) What is the Foreign Function Interface of the Coq Programming Language? (ITP) Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper)
F
factorization	(SCSC) EA: New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square
fairness	(FM) Encoding fairness in a synchronous concurrent program algebra
Fairness objectives	(CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives
false negative rate	(LearnAut) Toward Learning Boolean Functions from Positive Examples
false positive rate	(LearnAut) Toward Learning Boolean Functions from Positive Examples
Fan Theorem	(Domains13) A Brouwerian proof of the Fan Theorem
Fault tolerance	(FM) Resource-aware Design for Reliable Autonomous Applications with Multiple Periods
feasibility of functionals	(LICS) Type-two polynomial-time and restricted lookahead.
feature tree constraints	(IJCAR) Deciding the First-Order Theory of an Algebra of Feature Trees with Updates
fermionic quantum computing	(FSCD) A diagrammatic axiomatisation of fermionic quantum circuits
fibrancy of the function type	(HoTT/UF) Robust Notions of Contextual Fibrancy
fibrant replacement	(HoTT/UF) Robust Notions of Contextual Fibrancy
fibred category theory	(CL&C) The “duality of computation” from a fibrational perspective
field theory	(LCC) Computability over locally finite structures from algebra
Filter	(SAT) XORSAT Set Membership Filters
filter models	(HOR) Refining Properties of Filter Models: Sensibility, Approximability and Reducibility
Finite Automaton	(LaSh) Lazy Automata Techniques for WS1S
Finite model generator	(IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing
finite model property	(LICS) Unary negation fragment with equivalence relations has the finite model property
finite model theory	(LICS) Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth (LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
finite multisets	(Coq) Preliminary Report on the Yalla Library
Finite Semantics	(ICLP) Certified Graph View Maintenance with Regular Datalog
finite sum types	(LICS) Dialectica models of type theory
finitely partitioned trees	(LOLA) Heaps denote finitely partitioned trees
finitization	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points
Firmware	(CAV) Model Checking Boot Code from AWS Data Centers
first order theories	(Vampire) Experimenting with Theory Instantiation in Vampire
First order transduction	(LICS) Regular and First Order List Functions
first-order combinatorial proofs	(TYDI) Some incoherent musings on deep inference and combinatorial proofs
First-order list function	(LICS) Regular and First Order List Functions
first-order logic	(CAV) Model Generation for Quantified Formulas: A Taint-Based Approach (TYDI) Deep Inference, Herbrand's Theorem and Expansion Proofs (FM) Formal Specification and Verification of Dynamic Parametrized Architectures (Isabelle) Substitutionless First-Order Logic: A Formal Soundness Proof (SMT) What is the Point of an SMT-LIB Problem? (Vampire) Foundations of SPECTRE (PAAR) A Verified Simple Prover for First-Order Logic (PAAR) TFX: The TPTP Extended Typed First-order Form (PAAR) Set of Support for Higher-Order Reasoning (PAAR) Dynamic Strategy Priority: Empower the strong and abandon the weak (LCC) Traversal-invariant definability and Logarithmic-space computation (LICS) Separability by piecewise testable languages and downward closures beyond subwords (IJCAR) Efficient encodings of first-order Horn formulas in equational logic (IJCAR) Superposition with Datatypes and Codatatypes (IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (IJCAR) A Tableaux Calculus for Reducing Proof Size (HoTT/UF) First-order homotopical logic and Grothendieck fibrations (UITP) Partial Regularization of First-Order Resolution Proofs (VSTTE) Extending VIAP to Handle Array Programs (FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control
first-order logic with inductive definitions	(CL&C) Validating Back-links of FOL-ID Cyclic Pre-proofs
first-order logic with inductive predicates	(PARIS) Useless Explicit Induction Reasoning
First-order multiplicative linear logic	(LICS) Unification nets: canonical proof net quantifiers
First-Order Syntactic Unification	(UNIF) Formalization of First-Order Syntactic Unification
First-order Theory	(IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems
first-order theory of rewriting	(IJCAR) FORT 2.0
First-order types	(LICS) On the number of types in sparse graphs
Fishbone diagram	(GraMSec) Combining Bayesian Networks and Fishbone Diagrams to Distinguish between Intentional Attacks and Accidental Technical Failures
Fix-points	(HCVS) A simple functional presentation and an inductive correctness proof of the Horn algorithm
fixed parameter complexity	(MoRe) Parameterized complexity of games with monotonically ordered omega-regular objectives
fixed parameter tractable	(QBF) Tractability results for structured quantified CNF-formulas via knowledge compilation
Fixed Point Arithmetic	(SMT) The next 10^4 UppSAT Approximations
fixed point equations	(FSCD) Fixed-Point Constraints for Nominal Equational Unification
fixed points	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points
fixed-point algorithms for synthesis	(SYNT) Warm-Starting Fixed-Point Based Control Synthesis
fixed-point logic	(LICS) Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
Fixpoint Algorithms	(ICLP) Towards Incremental and Modular Context-sensitive Analysis
fixpoint alternation	(PARIS) Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic
fixpoint logic	(ARQNL) Evidence Extraction from Parameterised Boolean Equation Systems (LICS) A Fixpoint Logic and Dependent Effects for Temporal Property Verification
fixpoints	(Domains13) Invited Talk: Approximating partial by total: fixpoint characterizations of back-and-forth equivalences
flattener	(F-IDE) AsmetaF: a flattener for the ASMETA framework
Floating Point Arithmetic	(SMT) The next 10^4 UppSAT Approximations (IJCAR) Exploring Approximations for Floating-Point Arithmetic using UppSAT
floating-point	(SMT) Building Better Bit-Blasting for Floating-Point Problems
floating-point analysis	(FM) Combining Tools for Optimization and Analysis of Floating-Point Computations
floating-point optimization	(FM) Combining Tools for Optimization and Analysis of Floating-Point Computations
floating-point round-off errors	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
flocking	(VaVAS) Work-in-Progress: Adaptive Neighborhood Resizing for Stochastic Reachability in Distributed Flocking
Flow Analysis	(LICS) Causal Computational Complexity of Distributed Processes
flows and nowhere-zero flows	(LICS) A theory of linear typings as flows on 3-valent graphs
Fly-Automata	(LaSh) Monadic Second-Order Model Checking with Fly-Automata
FMI	(Overture) Multi-modelling of Cooperative Swarms
Focused Proof Systems	(IJCAR) A Logical Framework with Commutative and Non-Commutative Subexponentials
focused sequent calculus	(ARQNL) An Outline for Simple Semi-automated Proof Assistants for First-order Modal Logics (UITP) Interfacing with a Prover using Focusing and Logic Programming
focused sequent calculus for first-order modal logic	(ARQNL) An Outline for Simple Semi-automated Proof Assistants for First-order Modal Logics
Focusing	(LICS) Strong Sums in Focused Logic (LICS) Around Classical and Intuitionistic Linear Logics
Focussing	(IJCAR) Focussing, MALL and the polynomial hierarchy
FOIL algorithm	(ICLP) Cumulative Scoring-based Induction of Default Theories
FOL	(WiL) First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation
Forest Algebra	(LICS) MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras
Forest Algebras	(LICS) Wreath Products of Distributive Forest Algebras
Formal Analysis	(CSF) An extensive formal analysis of multi-factor authentication protocols
formal aspects of program analysis	(LICS) Work Analysis with Resource-Aware Session Types
Formal Definition	(LFMTP) What Does This Notation Mean Anyway? BNF-style notation as it is actually used
formal languages and automata theory	(CAV) Reactive Control Improvisation
Formal Library	(Coq) Classical Analysis with Coq
Formal Metatheory	(LFMTP) Formalisation of Barendregt's Variable Convention for Generic Structures with Binders (LFMTP) Formalization in Constructive Type Theory of the Standardization Theorem
Formal Methods	(DS-FM) A Formal Study of MANET Routing Protocols (CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (CAV) The DEEPSEC prover (FM) Disruptive Innovations for the Development and the Deployment of Fault-Free Software (FM) Z3 and SMT in Industrial R&D (FM) From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems (FM) CompoSAT: Specification-Guided Coverage for Model Finding (FM) The Compound Interest in Relaxing Punctuality (AVOCS) Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software (AVOCS) Analyzing Consistency of Formal Requirements (F-IDE) Integrating user design and formal models within PVSio-Web (F-IDE) The CLEAR Way To Transparent Formal Methods (F-IDE) Improving the Visualization of Alloy Instances (F-IDE) Experience Report on Formally Verifying Parts of OpenJDK's API with KeY (ITP) Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY (CSF) Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (VaVAS) Policing Functions for Machine Learning Systems (VSTTE) Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components (FCS) Homomorphisms and Minimality for Enrich-by-Need Security Analysis (SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions
formal methods for security	(CSF) Symbolic security of garbled circuits
formal methods in practice	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
Formal Model	(FCS) LISA: Predicting the Impact of DoS Attacks on Real-World Low Power IoT Systems
Formal proof	(AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base (CSF) Formal Security Proof of CMAC and its Variants
formal proofs	(Coq) Procrastination, A proof engineering technique (ITP) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs (ITP) Formalizing Ring Theory in PVS (Short Paper) (CSF) Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time”
formal reasoning	(ReMOTE) Elements of a Model of Trust in Technology
Formal Semantics	(NLCS) Propositional Forms of Judgemental Interpretations
formal specification	(FM) Formal Specification and Verification of Dynamic Parametrized Architectures (VEMDP) Executable Biochemical Space for Specification and Analysis of Biochemical Systems
formal topology	(LICS) Computable decision making on the reals and other spaces via partiality and nondeterminism
formal verification	(DS-FM) Formal verification of neural networks (FM) Interlocking Design Automation using Prover Trident (FM) Formal Specification and Verification of Dynamic Parametrized Architectures (FM) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (FM) Verifying Auto-Generated C Code from Simulink (SMT) SMT-based Compile-time Verification of Safety Properties for Smart Contracts (AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks (VEMDP) Using Transitivity and Modularity in Chemical Reaction Network Bisimulation (VEMDP) Formal Verification of Network-Based Biocomputation Circuits (LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (ITP) Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata (ITP) Verified Tail Bounds for Randomized Programs (CSF) Alethea: A Provably Secure Random Sample Voting Protocol (CSF) Computer-aided proofs for multiparty computation with active security (CSF) Composition Theorems for CryptoVerif and Application to TLS 1.3 (VaVAS) Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent (FCS) A Study on the Preservation on Cryptographic Constant-Time Security in the CompCert Compiler (FCS) Proving physical proximity using symbolic models
formal verification at runtime	(VaVAS) Towards a Hierarchical-Control Architecture for Distributed Autonomous Systems (Extended Abstract - Paper)
Formalisation	(ITP) An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory (VSTTE) Verified Certificate Checking for Counting Votes
formalization	(IWC) Certified Ordered Completion (IWC) Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL (UNIF) Formalization of First-Order Syntactic Unification (Isabelle) Substitutionless First-Order Logic: A Formal Soundness Proof (WiL) Can every real proof be represented by a formal proof? The Hilbert-Gentzen thesis (HDRA) Towards a fully formalized definition of syllepsis in weak higher categories
FormalVerification	(VEMDP) Bayesian Verification of Chemical Reaction Networks
forward proof-search	(EICNCL) A Forward Calculus for Countermodel Construction in IPL
four-valued logic	(GraMSec) On Linear Logic, Functional Programming, and Attack Trees
Frama-C	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
Frames	(Domains13) Frames and frame relations
Free choice sequences	(WiL) On Expanding Standard Notions of Constructivity
free modules	(IWC) The diamond lemma for free modules
free monad	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq
Free Variable	(LaSh) Lazy Automata Techniques for WS1S
Frege systems	(PC) Complexity of expander-based reasoning and the power of monotone proofs
Freyd categories	(Linearity/TLLA) From Linear Logic to Cyclic Sharing
Frobenius algebra	(LICS) Rewriting with Frobenius
FSM	(FM) FSM Inference from Long Traces
Full abstraction	(GS) A definable game semantics for the linear quantum lambda-calculus (LICS) Eager Functions as Processes
Function algebras	(LCC) A recursion-theoretic characterisation of the positive polynomial-time functions
Function classes	(LCC) A recursion-theoretic characterisation of the positive polynomial-time functions
function package	(ThEdu) Lucas Interpretation from Programmers’ Perspective
function summaries	(VSTTE) Lattice-Based Refinement in Bounded Model Checking
Functional Analysis	(LICS) A Logical Account for Linear Partial Differential Equations (Linearity/TLLA) Models of Linear Logic based on the Schwartz epsilon product
functional and relational specifications	(LFMTP) Computation-as-deduction in Abella: work in progress
functional dependency	(TERMGRAPH) Finding the Transitive Closure of Functional Dependencies using Strategic Port Graph Rewriting
Functional interpretation	(LICS) Dialectica models of type theory (LICS) A functional interpretation with state
Functional Mock-up Interface	(Overture) Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs
functional programming	(FSCD) Nominal Unification with Atom and Context Variables (FSCD) Counting Environments and Closures (LPOP) A software system should be declarative except where it interacts with the real world (LFMTP) Functional programming with λ-tree syntax: a progress report (GraMSec) On Linear Logic, Functional Programming, and Attack Trees (LICS) A Generalized Modality for Recursion (ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware (ITP) Formalization of a Polymorphic Subtyping Algorithm (VSTTE) Practical Methods for Reasoning about Java 8's Functional Programming Features (WPTE) Optimizing Space of Parallel Processes
functor	(ITP) Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes (FCS) A Homotopical Approach to Cryptography
functor algebra	(Domains13) Algebra semantics of recursive computation types
functorial spans	(LOLA) Asynchronous games fifteen years later
fuzz	(LICS) Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
fuzzer	(CAV) StringFuzz: A Fuzzer for String Solvers
fuzzy generalization	(UNIF) Proximity-Based Generalization
Fuzzy logic	(LICS) A van Benthem Theorem for Fuzzy Modal Logic
G
g-leakage	(FM) An Algebraic Approach for Reasoning About Information Flow
Game semantics	(PARIS) LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic (speaker: Pierre PRADIC) (GS) Automata Theory and Game Semantics (GS) Resource-Tracking Concurrent Games (GraMSec) The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement (LICS) Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (LICS) LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic (LICS) The concurrent game semantics of Probabilistic PCF (LICS) What's in a game? A theory of game models (LOLA) Asynchronous games fifteen years later
game theory	(LICS) Compositional game theory (MSFP) Backward induction for repeated games (ITP) Towards Formal Foundations for Game Theory (Short Paper)
Games	(SAT) Cops-Robber games and the resolution of Tseitin formulas
games and logic	(LICS) Distribution-based objectives for Markov Decision Processes
games played on finite graphs	(SR) Beyond admissibility: Dominance between chains of strategies
Gandy	(DCM) A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms
Gappa	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
garbled circuit	(CSF) Symbolic security of garbled circuits
generalised operads	(Domains13) Higher-dimensional categories: recursion on extensivity
generalised species	(LICS) Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs--
Generalization of syntactic parse trees	(NLCS) Anti-Unification and Natural Language Processing
Generalized Reactivity	(DS-FM) Heuristic-Based GR(1) Assumptions Refinement (FM) A Weakness Measure for GR(1) Formulae
Generic Binding Structures	(LFMTP) Formalisation of Barendregt's Variable Convention for Generic Structures with Binders
generic proof assistant	(UITP) Interfacing with a Prover using Focusing and Logic Programming
Genetic algorithms	(RCRA) An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
Geometric Automated Theorem Provers	(ThEdu) Rating of Geometric Automated Theorem Provers
geometric realization	(HoTT/UF) Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT
Geometry	(WiL) On Expanding Standard Notions of Constructivity
geometry of interaction	(DCM) Models of Computation that Conserve Data (LICS) The Geometry of Computation-Graph Abstraction (Linearity/TLLA) Coherent interaction graphs: a nondeterministic geometry of interaction for MLL
Gillespie algorithm	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems
Girard's translations	(Linearity/TLLA) The Bang Calculus and the Two Girard's Translations
global states	(CSF) A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif.
gluing	(LICS) Dialectica models of type theory
GNATProve	(WPTE) Verification of Ada Programs with AdaHorn
goal-directed evaluation	(ICLP) Constraint Answer Set Programming without Grounding
graded monads	(LOLA) Experimenting with graded monads: certified grading-based program transformations
Gradient Boosting on Decision Trees	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Gradient descent	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
Gradual Typing	(FSCD) Call-by-name Gradual Type Theory (ITRS) Gradual Intersection Types
grammar	(VSTTE) A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
Grammar testing	(NLCS) Automatic test suite generation for PMCFG grammars
Grammatical Framework	(ICLP-DC) Natural Language Generation From Ontologies (NLCS) Automatic test suite generation for PMCFG grammars (ICLP) Natural Language Generation From Ontologies: Application Paper
grammatical inference	(LearnAut) Learning Several Languages from Labeled Strings: State Merging and Evolutionary Approaches
graph	(SR) Concurrent games and semi-random determinacy
graph algorithms	(FSCD) Unique perfect matchings and proof nets
Graph Analysis	(LPOP) A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks
Graph Drawing	(LPOP) A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks
graph encoding	(TERMGRAPH) SLD-Resolution Reduction of Second-Order Horn Fragments - Extended Abstract
Graph Generation	(LPOP) A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks
graph grammars	(CAV) Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (TERMGRAPH) A framework for rewriting families of string diagrams
graph isomorphism	(LICS) Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
graph minor theorem	(ITP) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs
graph neural networks	(MLP) Deep Learning On Code with an Unbounded Vocabulary
Graph Queries	(ICLP) Certified Graph View Maintenance with Regular Datalog
Graph Recognition	(LPOP) A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks
Graph Representation	(LPOP) A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks
graph rewriting	(TERMGRAPH) Drags: an algebraic framework for graph rewriting (WST) GPO: A Path Ordering for Graphs (LOLA) A graph-rewriting perspective of the beta-law
graph rewriting systems	(TERMGRAPH) A Port-graph Model for Finance
graph theory	(LCC) Completeness in the Second Level of the Polynomial Time Hierarchy through Syntactic Properties (LICS) Allegories: decidability and graph homomorphisms (LICS) A theory of linear typings as flows on 3-valent graphs (ITP) A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs
Graph transformation	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems
Graph Views	(ICLP) Certified Graph View Maintenance with Regular Datalog
Graph Weighted Models	(LearnAut) Learning Graph Weighted Models on Pictures
graph-based characterization	(ICLP) MASP-Reduce: a proposal for distributed computation of stable models
Graphical reasoning	(LICS) Rewriting with Frobenius
Gray categories	(IWC) Critical pairs for Gray categories
Gray category	(FSCD) Coherence of Gray categories via rewriting
greatest fixed point	(CSF) Symbolic security of garbled circuits
Greedy Heuristics	(RCRA) Greedy Randomized Search for Scalable Compilation of Quantum Circuits
Groebner bases	(SCSC) EA: New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square
Grothendieck fibrations	(HoTT/UF) First-order homotopical logic and Grothendieck fibrations
Grothendieck quasi-topos	(Domains13) Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming
ground systems	(IWC) Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL
ground theories	(UNIF) ACUI Unification modulo Ground Theories
Grounding	(QBF) A Grounder From Second-Order Logic To QBF
Group decision	(PRUV) Evidential Group Decision Making Model with Belief-Based Preferences
Groupoid	(FCS) A Homotopical Approach to Cryptography
Gröbner Basis	(SCSC) RP: A Practical Polynomial Calculus for Arithmetic Circuit Verification
Guard Condition	(Coq) Towards a formalization of the guard condition
Guarded Recursion	(FSCD) The clocks they are adjunctions. Denotational semantics for Clocked Type Theory (PARIS) What makes guarded types tick? (LICS) Guarded Computational Type Theory (LICS) A Generalized Modality for Recursion
Guillotine Constraint	(RCRA) An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
H
Hadamard matrices	(SCSC) Hard Combinatorial Problems: A Challenge for Satisfiability
halting problem	(WST) Objective and Subjective Specifications (LICS) A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
Hamiltonian cycle	(POS) Stedman and Erin Triples encoded as a SAT Problem
hammers	(ITP) ProofWatch: Watchlist Guidance for Large Theories in E
Handlers	(LICS) Syntax and Semantics for Operations with Scopes
handwriting	(ITP) Towards Verified Handwritten Calculational Proofs (Short Paper)
Handwritten Digit Recognition	(ICLP) Incremental and Iterative Learning of Answer Set Programs from Mutually Distinct Examples
handwritten mathematics	(ITP) Towards Verified Handwritten Calculational Proofs (Short Paper)
hardness of approximation	(VEMDP) Computing properties of stable configurations of thermodynamic binding networks (VSTTE) Verification of Binarized Neural Networks via Inter-Neuron Factoring
Hardware model	(ITP) Physical Addressing on Real Hardware in Isabelle/HOL
hardware verification	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq (ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware
hardware-in-the-loop	(FM) Model-Based Testing for Avionics Systems
Hardware/software interfaces	(CAV) Model Checking Boot Code from AWS Data Centers
hash functions	(CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF
Hashing-based Algorithm	(PRUV) A New Probabilistic Algorithm for Approximate Model Counting
Haskell	(GraMSec) On Linear Logic, Functional Programming, and Attack Trees
HCI	(F-IDE) Improving the Visualization of Alloy Instances
head variable	(NLCS) Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus.
heaps	(LOLA) Heaps denote finitely partitioned trees
herbrand theorem	(SMT) Revisiting Enumerative Instantiation
Herbrand's theorem	(TYDI) Deep Inference, Herbrand's Theorem and Expansion Proofs (CL&C) Herbrand's Theorem as Higher-Order Recursion (CL&C) Fast cut-elimination using proof terms: an empirical study
hereditarily definable sets	(LICS) On computability and tractability for infinite sets
hereditary substitution	(MSFP) Everybody's Got To Be Somewhere
heuristic search	(DS-FM) Heuristic-Based GR(1) Assumptions Refinement
Heuristics	(ICLP-DC) Speeding Up Lazy-Grounding Answer Set Solving (RCRA) An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
hidden tree Markov model	(LearnAut) Learning Tree Distributions by Hidden Markov Models
Hierarchical information	(SR) Strategy Logic with Imperfect Information
Hierarchical state machines	(F-IDE) A Notebook Format for the Holistic Design of Embedded Systems
Hierarchy Theorem	(LICS) The State Complexity of Alternating Automata
higher categories	(IWC) Critical pairs for Gray categories (HoTT/UF) Towards the syntax and semantics of higher dimensional type theory
higher dimensional categories	(Domains13) Higher-dimensional categories: recursion on extensivity
Higher dimensional linear rewriting	(HDRA) Termination in linear (2,2)-categories with braidings and duals
higher groups	(LICS) Higher Groups in Homotopy Type Theory
higher inductive type	(HoTT/UF) Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT (FCS) A Homotopical Approach to Cryptography
higher inductive types	(FSCD) A Syntax for Higher Inductive-Inductive Types (LICS) On Higher Inductive Types in Cubical Type Theory (LICS) Impredicative Encodings of (Higher) Inductive Types
Higher order recursion schemes	(CL&C) Herbrand's Theorem as Higher-Order Recursion
higher-order	(Domains13) Robust computability notions for types arising in classical analysis
Higher-order abstract syntax (HOAS)	(LFMTP) Abstract Representation of Binders in OCaml using the Bindlib Library
higher-order computability	(LICS) Type-two polynomial-time and restricted lookahead.
higher-order logic	(WiL) Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task? (SMT) Higher-Order SMT Solving (Vampire) Developments in Higher-order Theorem proving within Vampire (PAAR) Set of Support for Higher-Order Reasoning (IJCAR) Superposition for Lambda-Free Higher-Order Logic (IJCAR) The Higher-Order Prover Leo-III
higher-order logic programming	(ARQNL) An Outline for Simple Semi-automated Proof Assistants for First-order Modal Logics (UITP) Interfacing with a Prover using Focusing and Logic Programming (ICLP) Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs
higher-order modal logic	(IJCAR) The Higher-Order Prover Leo-III
higher-order operads	(HOR) The next 700 (type-theoretical) denotational models ?
higher-order programs	(CAV) Propositional Dynamic Logic for Higher-Order Functional Programs (LICS) A Fixpoint Logic and Dependent Effects for Temporal Property Verification
higher-order reasoning	(IJCAR) The Higher-Order Prover Leo-III
higher-order recursion schemes	(FSCD) Homogeneity without Loss of Generality
higher-order rewriting	(WST) Termination of Lambda-Pi modulo rewriting using the size-change principle (HOR) Orthogonality and sequentiality in substructural Linear HRSs
higher-order term rewriting	(WST) Improving Static Dependency Pairs for Higher-Order Rewriting
higher-order unification	(FSCD) Nominal Unification with Atom and Context Variables
Higher-Ranked Polymorphism	(ITP) Formalization of a Polymorphic Subtyping Algorithm
Highly Assured Software	(FM) From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems
Hilbert's tenth problem	(Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Hilbert-Gentzen thesis	(WiL) Can every real proof be represented by a formal proof? The Hilbert-Gentzen thesis
HKDF	(CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF
HMAC	(CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF
HOL	(LFMTP) Sharing a library between proof assistants: reaching out to the HOL family (Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (IJCAR) The Higher-Order Prover Leo-III (ITP) Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata (VSTTE) Verified Certificate Checking for Counting Votes
HOL Light	(ITP) HOL Light QE
homogeneous	(IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems
homogeneous linear diophantine equations	(ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations
homogeneous types	(FSCD) Homogeneity without Loss of Generality
Homological algebra	(HDRA) Minimal models for monomial algebras
Homomorphism	(UNIF) Bounded ACh Unification
Homotopical algebra	(HDRA) Minimal models for monomial algebras
Homotopy	(FCS) A Homotopical Approach to Cryptography
homotopy type theory	(FSCD) A Syntax for Higher Inductive-Inductive Types (FSCD) Internal Universes in Models of Homotopy Type Theory (LICS) On Higher Inductive Types in Cubical Type Theory (LICS) Cellular Cohomology in Homotopy Type Theory (LICS) Free Higher Groups in Homotopy Type Theory (LICS) Higher Groups in Homotopy Type Theory (LICS) Impredicative Encodings of (Higher) Inductive Types (NLCS) Propositional Attitude Operators in Homotopy Type Theory (HoTT/UF) Cubical Computational Type Theory (HoTT/UF) Dependent Right Adjoint Types
Hopf Monad	(FSCD) Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
Horn clause	(PARIS) Coinductive Uniform Proofs: An Extended Abstract (speaker: Yue LI)
Horn Clause Transformation	(ICLP) Solving Horn Clauses on Inductive Data Types Without Induction
Horn clauses	(CAV) Constraint-Based Synthesis of Coupling Proofs (TERMGRAPH) SLD-Resolution Reduction of Second-Order Horn Fragments - Extended Abstract (HCVS) Towards Coinductive Theory Exploration in Horn Clause Logic: Extended Abstract (ICLP) Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
Horn propositional satisfiability algorithm	(HCVS) A simple functional presentation and an inductive correctness proof of the Horn algorithm
howe's method	(LICS) Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
HW-SW interface	(ITP) Physical Addressing on Real Hardware in Isabelle/HOL
hybrid logic	(LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
Hybrid System	(CAV) Spacetime Interpolants
hybrid system simulators	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction.
hybrid systems	(SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants (LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow
hydraulic oil pump	(FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty
Hyper sequents	(PARIS) Towards the Automatic Construction of Schematic Proofs
hypercube optimization	(PC) Optimization over the Boolean Hypercube via Sums of Nonnegative Circuit Polynomials
Hyperintensional Logic	(NLCS) Propositional Attitude Operators in Homotopy Type Theory
hyperltl	(SYNT) On the Expressiveness of HyperLTL Synthesis
hyperproperties	(CAV) Synthesizing Reactive Systems from Hyperproperties (CAV) Model Checking Quantitative Hyperproperties (SYNT) On the Expressiveness of HyperLTL Synthesis
Hyperproperty Verification	(CAV) Exploiting Synchrony and Symmetry in Relational Verification
Hypersequent calculus	(EICNCL) Hypersequent calculus for the logic of conditional belief: preliminary results
hypersequents	(Linearity/TLLA) Taking Linear Logic Apart
I
ic3	(SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses (AVOCS) A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways (SAT) Finding all Minimal Safe Inductive Sets
IDE	(ITP) Towards Verified Handwritten Calculational Proofs (Short Paper)
Idempontent	(UNIF) Towards Generalization Methods for Purely Idempotent Equational Theories
Idempotent quasigroups	(IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing
identifier	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Identity type	(FCS) A Homotopical Approach to Cryptography
IEEE-754	(SMT) Building Better Bit-Blasting for Floating-Point Problems
ILP	(TERMGRAPH) SLD-Resolution Reduction of Second-Order Horn Fragments - Extended Abstract
immunization	(CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF
imperative	(REFINE) a Theory of Lazy Imperative Timing
imperative calculi	(DCM) A syntactic model of mutation and aliasing
Imperative languages	(TERMGRAPH) Programming by Term Rewriting
imperative programming	(LPOP) A software system should be declarative except where it interacts with the real world
imperative programs	(WPTE) On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems
Imperfect information	(SR) Strategy Logic with Imperfect Information
Implementation and benchmarks for parity games	(SR) Solving Parity Games: Explicit vs Symbolic
implicate generation	(IJCAR) A Generic Framework for Implicate Generation Modulo Theories
implicative algebras	(ITP) Formalizing Implicative Algebras in Coq
implicit complexity	(FSCD) Term rewriting characterisation of LOGSPACE for finite and infinite data (LCC) A recursion-theoretic characterisation of the positive polynomial-time functions (Linearity/TLLA) A semantic conjecture on second-order MLL and its complexity consequences (work in progress)
Implicit Hitting Set	(IJCAR) Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories
Importance Splitting	(FM) Statistical Model Checking of LLVM Code
impredicative encodings	(LICS) Impredicative Encodings of (Higher) Inductive Types
impredicativity	(LICS) Impredicative Encodings of (Higher) Inductive Types
inconsistency measures	(PRUV) Measuring Disagreement among Knowledge Bases
inconsistency-tolerant reasoning	(PRUV) Measuring Disagreement among Knowledge Bases
Inconsistent Requirements Explanation	(DS-FM) Consistency Checking of Functional Requirements
increasing chains	(SR) Beyond admissibility: Dominance between chains of strategies
Incremental	(SCSC) RP: Towards Incremental Cylindrical Algebraic Decomposition in Maple
Incremental Analysis	(ICLP) Towards Incremental and Modular Context-sensitive Analysis
Incremental Maintenance	(ICLP) Certified Graph View Maintenance with Regular Datalog
Incremental SAT	(IJCAR) An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem
Indexed types	(FSCD) Index-Stratified Types
Indistinguishability	(CAV) Model checking indistinguishability of randomized security protocols
induction	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points (PARIS) Transitive Closure Logic: Infinitary and Cyclic Proof Systems (WiL) Non-well-founded proof system for Transitive Closure Logic
induction principle	(ITP) Efficient Mendler-Style Lambda-Encodings in Cedille
induction reasoning	(PARIS) Useless Explicit Induction Reasoning (CL&C) Validating Back-links of FOL-ID Cyclic Pre-proofs
induction rules	(PC)
inductive datatypes	(ITP) Efficient Mendler-Style Lambda-Encodings in Cedille
Inductive Definitions	(AVOCS) An Entailment Checker for Separation Logic with Inductive Definitions (HCVS) A simple functional presentation and an inductive correctness proof of the Horn algorithm
Inductive invariants	(CAV) Syntax-Guided Termination Analysis (SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses (CSF) Inductive Invariants for Noninterference in Multi-agent Workflows
Inductive Logic Programming	(ICLP-DC) The Learning-Knowledge-Reasoning Paradigm For Natural Language Understanding and Question Answering (ICLP) Exploiting Answer Set Programming with External Sources for Meta-Interpretive Learning (ICLP) Incremental and Iterative Learning of Answer Set Programs from Mutually Distinct Examples (ICLP) Learning Commonsense Knowledge through Interactive Dialogue (ICLP) Cumulative Scoring-based Induction of Default Theories
Inductive predicates	(ADSL) Labelled Cyclic Proofs for Separation Logic
inductive theorem prover	(PARIS) Towards the Automatic Construction of Schematic Proofs
Inductive Theorem Proving	(ICLP) Solving Horn Clauses on Inductive Data Types Without Induction
inductive types	(FSCD) Cumulative Inductive Types in Coq (LICS) Impredicative Encodings of (Higher) Inductive Types
inductive validity cores	(CAV) The JKind Model Checker
inductive-inductive types	(FSCD) A Syntax for Higher Inductive-Inductive Types
Industrial application	(Overture) Transforming an industrial case study from VDM++ to VDM-SL
industrial case	(FM) Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty
industrial impact	(FM) 20 Years of "Real" Real-Time Model Checking
inference	(FM) FSM Inference from Long Traces (NLCS) Automated Reasoning from Polarized Parse Trees
inference attacks	(CSF) Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting
infinitary and cyclic systems	(WiL) Non-well-founded proof system for Transitive Closure Logic
Infinitary Proofs	(PARIS) Transitive Closure Logic: Infinitary and Cyclic Proof Systems
infinitary rewriting	(FSCD) Strict Ideal Completions of the Lambda Calculus (FSCD) Term rewriting characterisation of LOGSPACE for finite and infinite data
Infinite computation	(CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs
infinite descent	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points (AVOCS) An Entailment Checker for Separation Logic with Inductive Definitions
infinite duration	(SR) Concurrent games and semi-random determinacy
Infinite modalities	(EICNCL) Sequent Calculi for Logic that Includes an Infinite Number of Modalities
infinite-state systems	(CAV) Eager Abstraction for Symbolic Model Checking (LICS) Separability by piecewise testable languages and downward closures beyond subwords
Infinite-valued logic	(ARQNL) Formalization of a Paraconsistent Infinite-Valued Logic
Infinitely nested Boolean structure	(CL&C) A Denotational Model of the Typed Lambda-Mu Calculus
Infinity-Categories	(HoTT/UF) (Truncated) Simplicial Models of Type Theory
Infinity-Presheaves	(HoTT/UF) (Truncated) Simplicial Models of Type Theory
informal proofs	(WiL) Can every real proof be represented by a formal proof? The Hilbert-Gentzen thesis
Information Disclosure Analysis	(GraMSec) Disclosure Analysis of SQL Workflows
Information Extraction	(MLP) Answering Cloze-style Software Questions Using Stack Overflow
information flow	(FM) Formal Specification and Verification of Dynamic Parametrized Architectures (LaSh) A Logic of Information Flows (LICS) A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (CSF) Assuming you know: epistemic semantics of relational annotations for expressive flow policies (CSF) Knowledge-based Security of Dynamic Secrets for Reactive Programs (CSF) A Permission-Dependent Type System for Secure Information Flow Analysis (CSF) The Complexity of Monitoring Hyperproperties
information flow analysis	(CAV) Lazy Self-Composition for Security Verification
Information flow control	(CSF) Types for Information Flow Control: Labeling Granularity and Semantic Models
Injectivity	(Domains13) Frames and frame relations
inner-approximations	(CAV) Inner and Outer Approximating Flowpipes for Delay Differential Equations
innermost conditional narrowing	(FSCD) Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems
Insider threat	(GraMSec) A state machine system for insider threat detection
instantiation	(SMT) Revisiting Enumerative Instantiation (SMT) Higher-Order SMT Solving (Vampire) Giving AVATAR Quantifiers to Play With
Integer Arithmetic	(IJCAR) A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
Integer Transition Systems	(WST) Complexity Analysis for Bitvector Programs
integer weights	(LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
Integrated Development Environment	(FM) QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems (F-IDE) User Support for the Combinator Logic Synthesizer Framework
integrated verification	(FM) Evidential and Continuous Integration of Software Verification Tools
Integration	(CAV) Continuous formal verification of Amazon s2n (FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems
integrity	(CSF) A Cryptographic Look at Multi-Party Channels
Intension	(NLCS) Propositional Attitude Operators in Homotopy Type Theory
intensional computation	(Domains13) Domain Theory for Intensional Computation
Intensional Logic	(NLCS) Propositional Attitude Operators in Homotopy Type Theory
Intensional Sets	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates
Intensional Type Theory	(NLCS) Propositional Attitude Operators in Homotopy Type Theory
Intentional attack	(GraMSec) Combining Bayesian Networks and Fishbone Diagrams to Distinguish between Intentional Attacks and Accidental Technical Failures
intentions	(ICLP) An ASP Methodology for Understanding Narratives about Stereotypical Activities
interaction graphs	(Linearity/TLLA) Coherent interaction graphs: a nondeterministic geometry of interaction for MLL
Interaction nets	(DCM) Models of Computation that Conserve Data
Interactive system	(F-IDE) Integrating user design and formal models within PVSio-Web
interactive theorem prover	(UITP) Automated Theorem Proving in a Chat Environment
interactive theorem proving	(ThEdu) Towards intuitive reasoning in axiomatic geometry (LaSh) A Derivative-Based Decision Procedure for WS1S (IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (F-IDE) Lightweight Interactive Proving inside an Automatic Program Verifier (ITP) Verified Memoization and Dynamic Programming (ITP) Software Tool Support for Modular Reasoning in Modal Logics of Actions (ITP) Towards Verified Handwritten Calculational Proofs (Short Paper)
interactive tool	(FSCD) ProTeM: A Proof Term Manipulator
Interface design	(F-IDE) Integrating user design and formal models within PVSio-Web
Interlocking	(FM) Interlocking Design Automation using Prover Trident (AVOCS) A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways
Intermediate Language for Verification	(F-IDE) Lightweight Interactive Proving inside an Automatic Program Verifier
intermediate representations	(LOLA) A more precise, more correct stack and register model for CompCert
internal and external calculi	(WiL) A semantical view of sequent based systems
Internal calculi	(EICNCL) Effective Translations between Display and Labelled Proofs for Tense Logics
internal language	(FSCD) Internal Universes in Models of Homotopy Type Theory
internal parametricity	(HoTT/UF) Internalizing Presheaf Semantics: Charting the Design Space
Internet of Things	(AVOCS) Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks (FCS) LISA: Predicting the Impact of DoS Attacks on Real-World Low Power IoT Systems
Interoperability	(LFMTP) Sharing a library between proof assistants: reaching out to the HOL family
Interpolation	(CAV) Spacetime Interpolants (CAV) Learning Abstractions for Program Synthesis (SMT) Selfless Interpolation for Infinite-State Model Checking (HCVS) Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions
Interpretable Machine Learning	(POS) MLIC: A MaxSAT-Based framework for learning interpretable classification rules
interprocedural analysis	(WST) Procedure-Modular Termination Analysis
Intersection Type Systems	(Linearity/TLLA) Generalized generalized species of structure and resource modalities
intersection types	(ITRS) Natural Deduction and Normalization Proofs for the Intersection Type Discipline (ITRS) Gradual Intersection Types (ITRS) Intersection Subtyping with Constructors (ITRS) (TYDI) Deep-Inference Intersection Types (LICS) Every λ-Term is Meaningful for the Infinitary Relational Model
intersections	(LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
interval arithmetics	(SCSC) EA: New in CoCoA-5.2.4 and CoCoALib-0.99570 for SC-Square
interval propagation	(SCSC) EA: Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT
Intrinsic noise	(VEMDP) Noise control for molecular computing
intruder deduction problem	(UNIF) Knowledge Problems in Equational Extensions of Subterm Convergent Theories
intuitionism	(Domains13) A Brouwerian proof of the Fan Theorem
intuitionistic combinatorial proofs	(TYDI) Some incoherent musings on deep inference and combinatorial proofs
intuitionistic linear logic	(FSCD) Proof nets for bi-intuitionistic linear logic (LICS) Around Classical and Intuitionistic Linear Logics (LOLA) Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic
Intuitionistic logic	(PC) Towards theories for positive polynomial time and monotone proofs with extension (LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic (CL&C) Admissible tools in the kitchen of intuitionistic logic (EICNCL) Intuitionistic multi-agent subatomic natural deduction for belief and knowledge (ICLP) First-order answer set programming as constructive proof search
Intuitionistic logic of constant domains	(CL&C) On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains
Intuitionistic mathematics	(WiL) On Expanding Standard Notions of Constructivity
Intuitionistic Modal Logic	(WiL) Decomposing labelled proof theory for intuitionistic modal logic (WiL) Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task? (EICNCL) Toward intuitionistic non-normal modal logic and its calculi
intuitionistic propositional logic	(EICNCL) A Forward Calculus for Countermodel Construction in IPL
Invariant Checking	(SYNT) On Inductive Verification and Synthesis
Invariant Generation	(CAV) Exploiting Synchrony and Symmetry in Relational Verification
Invariant Synthesis	(SYNT) On Inductive Verification and Synthesis
Invariants	(Vampire) Foundations of SPECTRE (F-IDE) A Notebook Format for the Holistic Design of Embedded Systems (SAT) Effective use of SMT solvers for Program Equivalence Checking through Invariant Sketching and Query Decomposition
Inverse Reinforcement Learning	(CAV) Safety-Aware Apprenticeship Learning
IRM-calc	(SAT) Local Soundness for QBF Calculi
irrelevance	(LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
Isabelle	(ThEdu) Lucas Interpretation from Programmers’ Perspective (Isabelle) Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (Isabelle) Further Scaling of Isabelle Technology (Isabelle) The remote_build Tool (LaSh) A Derivative-Based Decision Procedure for WS1S (IJCAR) Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle (UITP) Isabelle/PIDE after 10 years of development (ITP) Software Tool Support for Modular Reasoning in Modal Logics of Actions (ITP) Verified Analysis of Random Binary Tree Structures (ITP) Towards Formal Foundations for Game Theory (Short Paper)
Isabelle Proof Assistant	(UNIF) Formalization of First-Order Syntactic Unification (ThEdu) Proving in the Isabelle Proof Assistant that the Set of Real Numbers is not Countable (ThEdu) Students' Proof Assistant (SPA) (ThEdu) Natural Deduction Assistant (NaDeA)
Isabelle/HOL	(IWC) Certified Ordered Completion (ARQNL) Formalization of a Paraconsistent Infinite-Valued Logic (Isabelle) Formal Verification of Bounds for the LLL Basis Reduction Algorithm (Isabelle) PaMpeR: A Proof Method Recommendation System for Isabelle/HOL (PAAR) A Verified Simple Prover for First-Order Logic (IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (ITP) Verified Memoization and Dynamic Programming (ITP) Physical Addressing on Real Hardware in Isabelle/HOL (ITP) Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes (ITP) Fast Machine Words in Isabelle/HOL (ITP) A Formalization of the LLL Basis Reduction Algorithm (ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations (ITP) MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)
Isabelle/HOL Theorem Proving	(ITP) Program Verification in the Presence of Cached Address Translation
Isabelle/jEdit	(F-IDE) Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents
IsaSAT	(Isabelle) A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract)
Isomorphism type	(SAT) Minimal unsatisfiability and minimal strongly connected digraphs
isotopy	(HDRA) Normal forms for planar connected string diagrams
Iterated Boolean games	(SR) Local Equilibria in Logic-Based Multi-Player Games
J
JASP	(LPOP) Role-Based Access Control via JASP
Java	(CAV) JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (VSTTE) Practical Methods for Reasoning about Java 8's Functional Programming Features
Java byte-code	(VSTTE) A Java bytecode formalisation
JDLV	(LPOP) Invited Talk: On the Development of Industrial Applications with ASP
jEdit	(UITP) Isabelle/PIDE after 10 years of development
JML	(VSTTE) Practical Methods for Reasoning about Java 8's Functional Programming Features
Jordan Normal Form	(WST) A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving
Judgemental Interpretation	(NLCS) Propositional Forms of Judgemental Interpretations
Jung-Tix problem	(Domains13) Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming
Jupyter	(F-IDE) A Notebook Format for the Holistic Design of Embedded Systems
K
k-safety verification	(CAV) Lazy Self-Composition for Security Verification
Kachinuki order	(WST) Comparing on Strings: Semantic Kachinuki Order
Kakutani's fixed point theorem	(LICS) Distribution-based objectives for Markov Decision Processes
KeY	(F-IDE) Experience Report on Formally Verifying Parts of OpenJDK's API with KeY (ITP) Understanding Parameters of Deductive Verification: an Empirical Investigation of KeY
key set	(IJCAR) Automated Reasoning about Key Sets
kleptography	(CSF) Backdoored Hash Functions: Immunizing HMAC and HKDF (CSF) Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks
Knapsack	(SMT) Puli - A Problem-Specific OMT Solver
knot theory	(SCSC) RP: Unknot Recognition Through Quantifier Elimination
Knowledge Acquisition	(ICLP-DC) Knowledge Authoring and Question Answering via Controlled Natural Language
Knowledge and belief	(EICNCL) Intuitionistic multi-agent subatomic natural deduction for belief and knowledge
Knowledge based Reasoning	(FM) Timed Epistemic Knowledge Bases for Social Networks
knowledge compilation	(PC) Proof systems for #SAT based on restricted circuits (QBF) Tractability results for structured quantified CNF-formulas via knowledge compilation
Knowledge Representation	(LPOP) Logic-based Methods for Software Engineers and Business People (NLCS) Graph Knowledge Representations for SICK
Knowledge Representation and Reasoning	(ICLP-DC) The Learning-Knowledge-Reasoning Paradigm For Natural Language Understanding and Question Answering (ICLP-DC) Explaining Actual Causation via Reasoning about Actions and Change
knowledge-based noninterference	(CSF) Knowledge-based Security of Dynamic Secrets for Reactive Programs
Knuth-Bendix criterion	(UNIF) Rewriting with Generalized Nominal Unification
Koat	(WST) Control-Flow Refinement via Partial Evaluation
Kripke model	(EICNCL) Sequent Calculi for Logic that Includes an Infinite Number of Modalities
L
L-derivative	(Domains13) A logical view of complex analytic maps
Labelled calculi	(EICNCL) Proof theory for quantified monotone modal logics (EICNCL) Effective Translations between Display and Labelled Proofs for Tense Logics
labelled calculus	(EICNCL) Toward intuitionistic non-normal modal logic and its calculi
labelled Markov chain	(CAV) Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains
Labelled proof-systems	(ARQNL) Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic
labelled sequent calculi	(ARQNL) Labelled Calculi for QMLs with Non-Rigid and Non-Denoting Terms
Labelled sequents	(WiL) Decomposing labelled proof theory for intuitionistic modal logic
labelled systems	(WiL) A semantical view of sequent based systems
lambda calculi	(LICS) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
lambda calculus	(FSCD) Strict Ideal Completions of the Lambda Calculus (FSCD) On repetitive right application of B-terms (FSCD) Nominal Unification with Atom and Context Variables (ITRS) Strong normalization of simple types through uniform intersection types. (ITRS) Gradual Intersection Types (LPOP) A software system should be declarative except where it interacts with the real world (DCM) Towards a Formal System for Topological Quantum Computation (PARIS) Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic (LFMTP) Formalization in Constructive Type Theory of the Standardization Theorem (LICS) Probabilistic stable functions on discrete cones are power series. (LICS) Eager Functions as Processes (Linearity/TLLA) The Bang Calculus and the Two Girard's Translations (Linearity/TLLA) How to count linear and affine closed lambda terms? (HOR) Orthogonality and sequentiality in substructural Linear HRSs (ICLP) First-order answer set programming as constructive proof search
lambda calculus and combinatory logic	(LICS) A theory of linear typings as flows on 3-valent graphs
lambda prolog	(ARQNL) An Outline for Simple Semi-automated Proof Assistants for First-order Modal Logics
lambda-calculus	(FSCD) Counting Environments and Closures (FSCD) Homogeneity without Loss of Generality (ITRS) Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus (TYDI) Deep-Inference Intersection Types (TYDI) An introduction to deep inference (GS) A definable game semantics for the linear quantum lambda-calculus (WST) Termination of Lambda-Pi modulo rewriting using the size-change principle (LICS) Every λ-Term is Meaningful for the Infinitary Relational Model (Linearity/TLLA) On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants (HOR) Normalization and Taylor expansion of lambda-terms
lambda-encodings	(ITP) Efficient Mendler-Style Lambda-Encodings in Cedille
lambda-free higher-order logic	(IJCAR) Superposition for Lambda-Free Higher-Order Logic
lambda-prolog	(UITP) Interfacing with a Prover using Focusing and Logic Programming
lambda-tree syntax	(LFMTP) Functional programming with λ-tree syntax: a progress report
lambek calculus	(Linearity/TLLA) Substructural Calculi with Dependent Types (Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
lams	(FM) A lightweight deadlock analysis technique of object-oriented programs
language based security	(CSF) A Permission-Dependent Type System for Secure Information Flow Analysis
Language inclusion	(CAV) Automata vs Linear-Programming Discounted-Sum Inclusion
large libraries	(ITP) ProofWatch: Watchlist Guidance for Large Theories in E
Large set	(IJCAR) Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing
large theories	(IJCAR) An abstraction-refinement framework for reasoning with large theories
large-scale reasoning	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description
lattice	(VSTTE) Lattice-Based Refinement in Bounded Model Checking
Lattice Basis Reduction	(Isabelle) Formal Verification of Bounds for the LLL Basis Reduction Algorithm
lattice traversal	(VSTTE) Lattice-Based Refinement in Bounded Model Checking
lax homomorphism	(Domains13) Algebra semantics of recursive computation types
laziness	(LICS) A sequent calculus with dependent types for classical arithmetic
lazy	(REFINE) a Theory of Lazy Imperative Timing
lazy evaluation	(Isabelle) Lazy Algebraic Types in Isabelle/HOL
lazy grounding	(ICLP-DC) Speeding Up Lazy-Grounding Answer Set Solving
lazy self-composition	(CAV) Lazy Self-Composition for Security Verification
Lean proof assistant	(LICS) Higher Groups in Homotopy Type Theory
learning	(CAV) The Learnability of Symbolic Automata (SYNT) Minimal Synthesis of String To String Functions From Examples
Learning from positive examples	(LearnAut) Toward Learning Boolean Functions from Positive Examples
learning transductions	(LearnAut) Learning Tree Distributions by Hidden Markov Models
Learning Weighted Automata	(LearnAut) Learning Graph Weighted Models on Pictures
learning-based testing	(LearnAut)
Least general generalization	(FSCD) Term-Graph Anti-Unification (NLCS) Anti-Unification and Natural Language Processing
Lemma learning	(SMT) Proofs in conflict-driven theory combination
lens	(MSFP) Profunctor Optics and the Yoneda Lemma
Leo-III	(IJCAR) The Higher-Order Prover Leo-III
Leveled sequents	(PARIS) Towards the Automatic Construction of Schematic Proofs
LFSR	(POS) Stedman and Erin Triples encoded as a SAT Problem
Likelihood weighting	(ICLP) Constraint-Based Inference in Probabilistic Logic Programs
Lina	(GraMSec) On Linear Logic, Functional Programming, and Attack Trees
linear algorithm	(POS) Local-Style Search in the Linear MaxSAT Algorithm: A Computational Study of Solution-Based Phase Saving
Linear Arithmetic	(IJCAR) A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
Linear categories	(HDRA) Termination in linear (2,2)-categories with braidings and duals
Linear Category	(FSCD) Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
linear clauses	(SCSC) RP: Refutation of Products of Linear Polynomials
linear cliquewidth	(LICS) Definable decompositions for graphs of bounded linear cliquewidth
Linear Constraints	(IJCAR) Checking Array Bounds by Abstract Interpretation and Symbolic Expressions
linear distributivity	(TYDI) Some incoherent musings on deep inference and combinatorial proofs
linear logic	(FSCD) Proof nets for bi-intuitionistic linear logic (FSCD) Unique perfect matchings and proof nets (ITRS) Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus (TYDI) Some incoherent musings on deep inference and combinatorial proofs (PARIS) LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic (speaker: Pierre PRADIC) (PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points (ARQNL) Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic (GraMSec) The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement (GraMSec) On Linear Logic, Functional Programming, and Attack Trees (LICS) LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic (LICS) The Syntax and Semantics of Quantitative Type Theory (LICS) Unification nets: canonical proof net quantifiers (LICS) Work Analysis with Resource-Aware Session Types (LICS) Around Classical and Intuitionistic Linear Logics (LICS) A theory of linear typings as flows on 3-valent graphs (IJCAR) Focussing, MALL and the polynomial hierarchy (Coq) Preliminary Report on the Yalla Library (Linearity/TLLA) Generalized generalized species of structure and resource modalities (Linearity/TLLA) The structure of non decomposable connectives of linear logic (Linearity/TLLA) Substructural Calculi with Dependent Types (Linearity/TLLA) Formalization of Automated Trading Systems in a Concurrent Linear Framework (Linearity/TLLA) Benchmarking Linear Logic Translations (Linearity/TLLA) The Bang Calculus and the Two Girard's Translations (Linearity/TLLA) On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants (Linearity/TLLA) From Linear Logic to Cyclic Sharing (Linearity/TLLA) Taking Linear Logic Apart (Linearity/TLLA) On the Lambek Calculus with an Exchange Modality (HOR) Orthogonality and sequentiality in substructural Linear HRSs (HOR) Normalization and Taylor expansion of lambda-terms (LOLA) A resource modality for RAII (ICLP) A New Proof-theoretical Linear Semantics for CHR
Linear polygraphs	(HDRA) Termination in linear (2,2)-categories with braidings and duals
Linear Programming	(ITP) A Coq Tactic for Equality Learning in Linear Arithmetic
Linear Temporal Logic	(DS-FM) Consistency Checking of Functional Requirements (CAV) Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (CAV) Strix: Explicit Reactive Synthesis Strikes Back! (SYNT) Warm-Starting Fixed-Point Based Control Synthesis (SYNT) Reactive Synthesis from LTL Specification with Spot (LICS) One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata (LICS) Automaton-Based Criteria for Membership in CTL (SR) Local Equilibria in Logic-Based Multi-Player Games (ICLP) Temporal Answer Set Programming on Finite Traces
linear term	(Linearity/TLLA) How to count linear and affine closed lambda terms?
linear time hierarchy	(LICS) A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
Linear Transformations	(IJCAR) A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
Linear Tree Constraints	(LaSh) Decidable Linear Tree Constraints
linear-feedback shift register	(POS) Stedman and Erin Triples encoded as a SAT Problem
linear/non-linear logic	(Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
Linearity	(DCM) Models of Computation that Conserve Data
linearizability	(CAV) Monitoring Weak Consistency
Linearization	(SMT) The next 10^4 UppSAT Approximations
Lipschitz maps	(Domains13) A logical view of complex analytic maps
Lists	(ADSL) The Complexity of Prenex Separation Logic with One Selector
Literate programming	(F-IDE) A Notebook Format for the Holistic Design of Embedded Systems
Liveness Analysis	(CAV) Symbolic Liveness Analysis of Real-World Software
LLVM	(CAV) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (FM) Statistical Model Checking of LLVM Code
Local determinism	(DCM) A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms
Local Theory Extensions	(SYNT) On Inductive Verification and Synthesis
locale theory	(LICS) Computable decision making on the reals and other spaces via partiality and nondeterminism
Log analysis	(CSF) The Complexity of Monitoring Hyperproperties
logarithmic space computation	(LCC) Traversal-invariant definability and Logarithmic-space computation
logic	(TYDI) Nested sequents for modal logics and beyond (SCSC) RP: Unknot Recognition Through Quantifier Elimination (FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (LaSh) A Logic of Information Flows (LCC) A recursion-theoretic characterisation of the positive polynomial-time functions (LICS) Logics for Word Transductions with Synthesis
logic for PTime	(LICS) On computability and tractability for infinite sets
Logic for Teaching	(ThEdu) Towards intuitive reasoning in axiomatic geometry
Logic Meta-Programming	(LPOP) LPOP2018 XSB Position Paper
Logic of Here and There	(ICLP) Temporal Answer Set Programming on Finite Traces
Logic on Trees	(LICS) Wreath Products of Distributive Forest Algebras
logic program	(ASPOCP) Partial Evaluation of Logic Programs in Vector Spaces
logic programming	(LPOP) LPOP2018 XSB Position Paper (FM) Variant Analysis with QL (ASPOCP) A Survey of Advances in Epistemic Logic Program Solvers (ASPOCP) Syntactic Conditions for Antichain Property in Consistency Restoring Prolog (ASPOCP) Datalog for Static Analysis Involving Logical Formulae (VEMDP) Rule-based design of computational DNA devices (IJCAR) Focussing, MALL and the polynomial hierarchy (RCRA) Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic (RCRA) Externally Supported Models for Efficient Computation of Paracoherent Answer Sets (ICLP) Top-down and Bottom-up Evaluation Procedurally Integrated (ICLP) Epistemic Logic Programs with World View Constraints
Logic Programming Applications	(RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper)
Logic Solvers	(CAV) Understanding and Extending Incremental Determinization for 2QBF
Logic Tools	(ThEdu) Students' Proof Assistant (SPA) (ThEdu) Natural Deduction Assistant (NaDeA)
Logic-based tools	(ICLP-DC) Model Revision of Logical Regulatory Networks using Logic-based Tools
Logical complexity	(PARIS) On the Logical Complexity of Cyclic Arithmetic
logical design	(TERMGRAPH) Finding the Transitive Closure of Functional Dependencies using Strategic Port Graph Rewriting
logical formalism	(FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control
logical framework	(Linearity/TLLA) Formalization of Automated Trading Systems in a Concurrent Linear Framework
Logical Frameworks	(LFMTP) Sharing a library between proof assistants: reaching out to the HOL family (LICS) Strong Sums in Focused Logic (IJCAR) A Logical Framework with Commutative and Non-Commutative Subexponentials
Logical models	(WST) Well-founded models in proofs of termination
logical paradoxes	(LICS) Logical paradoxes in quantum computation
logical predicates	(LICS) Dialectica models of type theory
Logical Regulatory Networks	(ICLP-DC) Model Revision of Logical Regulatory Networks using Logic-based Tools
Logical relations	(FSCD) A Syntax for Higher Inductive-Inductive Types (FSCD) Index-Stratified Types
logically constrained term rewriting systems	(IJCAR) A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems
Logics for strategic reasoning	(SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions
Logistics	(ICLP-DC) Scalable Robotic Intra-Logistics with Answer Set Programming
LOGSPACE	(FSCD) Term rewriting characterisation of LOGSPACE for finite and infinite data
LOIS	(LICS) On computability and tractability for infinite sets
long-distance resolution	(SAT) Local Soundness for QBF Calculi
loop unrolling	(ITP) Verified Timing Transformations in Synchronous Circuits with LambdaPi-Ware
loops	(VSTTE) Loop Detection by Logically Constrained Term Rewriting
low-level language	(VSTTE) A Java bytecode formalisation
Lower Bounds	(PC) Resolution with Counting: Different Moduli and Tree-Like Lower Bounds (PC) Resolution and the binary encoding of combinatorial principles (LICS) The State Complexity of Alternating Automata
LPMLN	(ICLP-DC) Probabalistic Action Language pBC+ (ICLP) A Probabilistic Extension of Action Language BC+
LPOD	(ICLP-DC) Translating P-log, LP^{MLN}, LPOD, and CR-Prolog2 into Standard Answer Set Programs (ICLP) Translating LPOD and CR-Prolog2 into Standard Answer Set Programs
LTI systems	(SYNT) Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants
LTLf	(WiL) First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation
lucas interpretation	(ThEdu) Lucas Interpretation from Programmers’ Perspective
Lukasiewicz Logics	(IJCAR) Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic
M
MAC	(CSF) Formal Security Proof of CMAC and its Variants
machine checked proofs	(IJCAR) Well-Founded Unions
Machine Ethics	(ReMOTE) Moral Permissibility of Actions in Smart Home Systems
Machine Learning	(CAV) Fast Numerical Program Analysis with Reinforcement Learning (Isabelle) PaMpeR: A Proof Method Recommendation System for Isabelle/HOL (IJCAR) A SAT-Based Approach to Learn Explainable Decision Sets (IJCAR) ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback (Coq) Proof Construction by Tactic Learning (MLP) Answering Cloze-style Software Questions Using Stack Overflow (MLP) Deep Learning On Code with an Unbounded Vocabulary (MLP) Measuring software development productivity: a machine learning approach (SAT) Machine Learning-based Restart Policy for CDCL SAT Solvers (CSF) Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting (ICLP) Cumulative Scoring-based Induction of Default Theories
Machine Learning Systems	(VaVAS) Policing Functions for Machine Learning Systems
machine words	(ITP) Fast Machine Words in Isabelle/HOL
magic states	(LICS) Logical paradoxes in quantum computation
Magic wand	(ADSL) The Complexity of Prenex Separation Logic with One Selector
MANET	(DS-FM) A Formal Study of MANET Routing Protocols
Maple	(SCSC) EA: SMT-like Queries in Maple
MapReduce	(ICLP) MASP-Reduce: a proposal for distributed computation of stable models
MapReduce framework	(VSTTE) Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
MARCO	(SAT) Finding all Minimal Safe Inductive Sets
Markov Decision Process	(MoRe) Logically-Constrained Reinforcement Learning (MoRe) Safe and Optimal Scheduling of Hard and Soft Tasks
Markov decision processes	(MoRe) Multiple Objectives and Cost Bounds in MDP (MoRe) Multi-Scenario Uncertainty in Markov Decision Processes (CAV) Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (CAV) Sound Value Iteration (CAV) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (LICS) Distribution-based objectives for Markov Decision Processes (LICS) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes (LICS) Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes (ITP) MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper) (VaVAS) Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot
Markov processes	(LICS) An algebraic theory of Markov processes
Martin-L\"{o}f type theory	(LICS) Impredicative Encodings of (Higher) Inductive Types
Martin-Löf type theory	(LICS) Dialectica models of type theory
Mason's Marks	(LPOP) A Rule-Based Tool for Analysis and Generation of Graphs Applied to Mason's Marks
Master Theorem	(ITP) Verified Tail Bounds for Randomized Programs
matching representation	(Domains13) T^\omega-representations of compact sets through dyadic subbases
mathematical analysis	(FSCD) Counting Environments and Closures
Mathematical Induction	(VSTTE) Extending VIAP to Handle Array Programs
Mathematical language	(UITP) Text-Orientated Formal Mathematics
mathematical proof	(ITP) Towards Verified Handwritten Calculational Proofs (Short Paper)
mathematical proofs	(WiL) Can every real proof be represented by a formal proof? The Hilbert-Gentzen thesis
Mathematics	(ITP) An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory
Matita	(LFMTP) Sharing a library between proof assistants: reaching out to the HOL family
Matrix Growth	(WST) A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving
Matrix Interpretation	(WST) A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving
Matrix semigroups	(LICS) Polynomial Invariants for Affine Programs
Maude	(FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols
maximum realizability	(SYNT) Maximum Realizability for Linear Temporal Logic Specifications
Maximum Satisfiability	(IJCAR) Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories
MaxSAT	(SYNT) Maximum Realizability for Linear Temporal Logic Specifications (POS) Local-Style Search in the Linear MaxSAT Algorithm: A Computational Study of Solution-Based Phase Saving (POS) MLIC: A MaxSAT-Based framework for learning interpretable classification rules (SAT) Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT (SAT) Solving MaxSAT with Bit-Vector Optimization
MAXSAT application	(SAT) Approximately Propagation Complete and Conflict Propagating Constraint Encodings
MaxSAT resolution	(PC) On Dual-Rail Based MaxSAT Solving
MaxSAT solving	(PC) On Dual-Rail Based MaxSAT Solving
maxSMT	(IJCAR) MaedMax: A Maximal Ordered Completion Tool
MC-SAT	(SMT) Centralizing Equality Reasoning in MCSAT
MCMT	(IJCAR) Cubicle-W: Parameterized Model Checking on Weak Memory
mealy machine	(SYNT) Minimal Synthesis of String To String Functions From Examples
mean-payoff games	(LICS) A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (SR) Infinite-Duration Richman Bidding Games
meaningless terms	(FSCD) Strict Ideal Completions of the Lambda Calculus
Measure theory	(GS) Continuous probability distributions in concurrent games
mechanical reasoning	(CL&C) Validating Back-links of FOL-ID Cyclic Pre-proofs
mechanised theorem proving	(LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic
mechanized mathematics	(ITP) A Formally Verified Solver for Homogeneous Linear Diophantine Equations
mechanized meta-theory	(LFMTP) Property-Based Testing of Abstract Machines: an Experience Report
Mechanized proofs	(WiL) Towards a Playground for Logicians
mechanized reasoning	(LICS) Cellular Cohomology in Homotopy Type Theory
Memoization	(ITP) Verified Memoization and Dynamic Programming
Memory	(ITP) Physical Addressing on Real Hardware in Isabelle/HOL
Memory consistency models	(PLR) RTLCheck: Automatically Verifying the Memory Consistency of Processor RTL (VSTTE) Store Buffer Reduction in The Presence of Mixed-Size Accesses and Misalignment
Memory Errors	(ICLP) Shape Neutral Analysis of Graph-based Data-structures
memory isolation	(AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base
memory model	(FM) Operational Semantics of a Weak Memory Model with Channel Synchronization
message passing concurrency	(CAV) On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony
Message Passing Interface	(FM) Dynamic Symbolic Verification of MPI Programs
meta programming	(ITP) Tactics and Certificates in Meta Dedukti
meta-data library	(POS) A Problem Meta-Data Library for Research in SAT
Meta-Interpretive Learning	(ICLP) Exploiting Answer Set Programming with External Sources for Meta-Interpretive Learning
meta-programming	(ITP) Towards Certified Meta-Programming with Typed Template-Coq
Meta-theory	(WiL) Towards a Playground for Logicians
Metamorphic Testing	(VaVAS) Policing Functions for Machine Learning Systems
Metareasoning	(ITP) HOL Light QE
metatheory	(HoTT/UF) Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT
Metric Semantics	(Domains13) Abstractness of Continuation Semantics for Asynchronous Concurrency
Minimal models	(HDRA) Minimal models for monomial algebras
Minimal unsatisfiability	(SAT) Minimal unsatisfiability and minimal strongly connected digraphs
Minimally Adequate Teacher	(LearnAut) Decision problems for Clark-congruential languages
Minimally strongly connected digraph	(SAT) Minimal unsatisfiability and minimal strongly connected digraphs
Minimisation	(IJCAR) An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem
Minsky machines	(LOLA) Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic
MIPS TLB	(ITP) Physical Addressing on Real Hardware in Isabelle/HOL
Mixed Arithmetic	(IJCAR) A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
Mixed Distributive Law	(FSCD) Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
Mixed Integer Linear Programming	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network
ML	(IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (VSTTE) Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications
MMSNP	(LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
Mobile robotics	(VaVAS) Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot
modal fixpoint logic	(PARIS) Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic
modal logic	(ARQNL) System Demonstration: The Higher-Order Prover Leo-III (LICS) A van Benthem Theorem for Fuzzy Modal Logic (LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic (IJCAR) An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem (IJCAR) The Higher-Order Prover Leo-III
Modal Logics	(WiL) On the Combination of Resolution and SAT Procedures for Modal Theorem-Proving (IJCAR) A Resolution-Based Calculus for Preferential Logics
modal mu	(LICS) A modal mu perspective on solving parity games in quasipolynomial time.
modal mu calculus	(ARQNL) Evidence Extraction from Parameterised Boolean Equation Systems
Modal type theory	(NLCS) Propositional Attitude Operators in Homotopy Type Theory (HoTT/UF) Dependent Right Adjoint Types
modalities	(FSCD) Internal Universes in Models of Homotopy Type Theory (LICS) Guarded Computational Type Theory (Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
Model Animation	(FM) From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems
model checking	(CAV) Propositional Dynamic Logic for Higher-Order Functional Programs (CAV) Model Checking Quantitative Hyperproperties (CAV) BTOR2, BtorMC and Boolector 3.0 (CAV) The JKind Model Checker (CAV) Monitoring CTMCs By Multi-Clock Timed Automata (CAV) On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (CAV) Eager Abstraction for Symbolic Model Checking (CAV) Model Checking Boot Code from AWS Data Centers (CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (CAV) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (CAV) Constrained Dynamic Partial Order Reduction (CAV) Attracting Tangles to Solve Parity Games (FM) 20 Years of "Real" Real-Time Model Checking (FM) SDN-Actors: Modeling and Verification of SDN Programs (FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems (FM) Verifying Auto-Generated C Code from Simulink (FM) Stepwise Development and Model Checking of a Distributed Interlocking System - using RAISE (FM) View abstraction for systems with component identities (FM) Producing Explanations for Rich Logics (LaSh) Monadic Second-Order Model Checking with Fly-Automata (ASPOCP) Datalog for Static Analysis Involving Logical Formulae (SMT) Selfless Interpolation for Infinite-State Model Checking (AVOCS) Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation (ReMOTE) Moral Permissibility of Actions in Smart Home Systems (LICS) Distribution-based objectives for Markov Decision Processes (ITP) Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata (VaVAS) RoboTool: Modelling and Verification with RoboChart (SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions (SR) Quantifying Bounds in Strategy Logic (SR) Strategy Logic with Imperfect Information (WPTE) Verification of Ada Programs with AdaHorn
Model Checking Games	(LaSh) Courcelle’s Theorem – A Game-Theoretic Approach
model construction	(IJCAR) Efficient Model Construction for Horn Logic with VLog: System Description
Model Counting	(CAV) Model Checking Quantitative Hyperproperties (IJCAR) A New Probabilistic Algorithm for Approximate Model Counting (SAT) Fast and Flexible Probabilistic Model Counting (PRUV) VolCE: An Efficient Tool for Solving #SMT(LA) Problems (PRUV) A New Probabilistic Algorithm for Approximate Model Counting
Model Expansion	(PRUV) A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems
model finding	(FM) CompoSAT: Specification-Guided Coverage for Model Finding
model generation	(CAV) Model Generation for Quantified Formulas: A Taint-Based Approach
Model learning	(FM) Towards `Verifying' a Water Treatment System
Model quality	(ICLP) Improving Candidate Quality of Probabilistic Logic Models
Model Revision	(ICLP-DC) Model Revision of Logical Regulatory Networks using Logic-based Tools
model sampling	(SAT) Fast Sampling of Perfectly Uniform Satisfying Assignments
model theory	(LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP (PRUV) A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems
Model transformations	(Overture) Transforming an industrial case study from VDM++ to VDM-SL
model-based engineering	(FM) IPL: An Integration Property Language for Multi-Model Cyber-Physical Systems
model-based testing	(FM) Model-Based Testing for Avionics Systems (ITP) Fast Machine Words in Isabelle/HOL
model-checking	(FM) Timed Vacuity (VaVAS) Social Consequence Engines (Abstract)
Model-checking first-order logic	(LICS) Parameterized circuit complexity of model-checking on sparse structures
model-checking problems	(LICS) Tree depth, quantifier elimination, and quantifier rank
Model-level uncertainty	(MoRe) Multi-Scenario Uncertainty in Markov Decision Processes
Modeling	(VEMDP) Rule-based design of computational DNA devices
Modeling and Specification	(CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine
Modelling Languages	(QBF) A Grounder From Second-Order Logic To QBF
modelling secure protocols	(CSF) Computer-aided proofs for multiparty computation with active security
models	(IJCAR) Theories as Types
Models of computation	(DCM) A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms
Modular Analysis	(ICLP) Towards Incremental and Modular Context-sensitive Analysis
modular approach	(FM) Modular Verification of Programs with Effects and Effect Handlers in Coq
Modular Arithmetic	(CAV) Formally Verified Montgomery Multiplication
Modular System	(LaSh) A Logic of Information Flows
Modular Tensor Category	(DCM) Towards a Formal System for Topological Quantum Computation
modules	(LICS) Strong Sums in Focused Logic
Molecular computing	(VEMDP) Noise control for molecular computing
Molecular Filters	(VEMDP) Molecular Filters for Noise Reduction
Molecular programming	(VEMDP) Rule-based design of computational DNA devices
monad	(LICS) Syntax and Semantics for Operations with Scopes (MSFP) Relating Idioms, Arrows and Monads from Monoidal Adjunctions (Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
Monadic Second Order Logic	(LaSh) Courcelle’s Theorem – A Game-Theoretic Approach (LaSh) Monadic Second-Order Model Checking with Fly-Automata
Monads	(NLCS) Propositional Attitude Operators in Homotopy Type Theory (Coq) What is the Foreign Function Interface of the Coq Programming Language? (MSFP) Some No-Go Theorems for Distributive Laws (extended abstract)
monitoring	(LICS) A Theory of Register Monitors
monoid	(MSFP) Relating Idioms, Arrows and Monads from Monoidal Adjunctions
monoid model	(Domains13) A Brouwerian proof of the Fan Theorem
monoidal categories	(FSCD) A diagrammatic axiomatisation of fermionic quantum circuits (LICS) Compositional game theory (LICS) Two complete axiomatisations of pure-state qubit quantum computing (HDRA) Normal forms for planar connected string diagrams (Linearity/TLLA) From Linear Logic to Cyclic Sharing
monoidal category	(MSFP) Relating Idioms, Arrows and Monads from Monoidal Adjunctions
Monoidal Coalgebra Modality	(FSCD) Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
monotone	(PC) Complexity of expander-based reasoning and the power of monotone proofs
Monotone complexity	(PC) Towards theories for positive polynomial time and monotone proofs with extension (LCC) A recursion-theoretic characterisation of the positive polynomial-time functions
Monotone proofs	(PC) Towards theories for positive polynomial time and monotone proofs with extension
monotonicity	(NLCS) Automated Reasoning from Polarized Parse Trees
Montague semantics	(NLCS) Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda calculus.
Montgomery Multiplication	(CAV) Formally Verified Montgomery Multiplication
MPI	(DS-FM) Analysis and Verification of Message Passing based Parallel Programs
MSO	(WiL) First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation (LaSh) A Derivative-Based Decision Procedure for WS1S (LaSh) Monadic Second-Order Model Checking with Fly-Automata (LICS) MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras
MSO on Infinite Words	(PARIS) LMSO: A Curry-Howard Approach to Church’s Synthesis via Linear Logic (speaker: Pierre PRADIC)
MSO on omega-Words	(LICS) LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic
MSO transduction	(LICS) Regular and First Order List Functions
mu-calculus	(FM) Producing Explanations for Rich Logics
mu-mutilde-calculus	(CL&C) The “duality of computation” from a fibrational perspective
Multi Factor	(CSF) An extensive formal analysis of multi-factor authentication protocols
Multi Modal logic	(EICNCL) Sequent Calculi for Logic that Includes an Infinite Number of Modalities
Multi-agent models	(EICNCL) Hypersequent calculus for the logic of conditional belief: preliminary results
Multi-agent Systems	(SR) Verification of Multi-agent Systems with Imperfect Information and Public Actions (SR) Local Equilibria in Logic-Based Multi-Player Games
Multi-agent workflows	(CSF) Inductive Invariants for Noninterference in Multi-agent Workflows
Multi-clock timed automata	(CAV) Monitoring CTMCs By Multi-Clock Timed Automata
Multi-dimensional	(VSTTE) Extending VIAP to Handle Array Programs
Multi-graphs	(TERMGRAPH) Drags: an algebraic framework for graph rewriting
multi-modelling	(Overture) Multi-modelling of Cooperative Swarms (Overture) Design Space Exploration for Secure Building Control
multi-objective optimization	(LICS) Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
Multi-objective synthesis	(MoRe) Safe and Optimal Scheduling of Hard and Soft Tasks
Multi-party computation	(CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
Multi-Pass Dynamic Programming	(SAT) Exploiting Treewidth for Projected Model Counting and its Limits
Multi-player games	(SR) Local Equilibria in Logic-Based Multi-Player Games
Multi-Robot planning	(FM) Multi-Robot LTL Planning Under Uncertainty
Multi-valued Logic	(IJCAR) Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic
multicategories	(HDRA) Merge-bicategories: towards semi-strictification of higher categories
multiplayer games	(MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives
multiple languages	(LearnAut) Learning Several Languages from Labeled Strings: State Merging and Evolutionary Approaches
multiplicative linear logic	(Linearity/TLLA) Proof nets, coends and the Yoneda isomorphism
Multiplier Verification	(SCSC) RP: A Practical Polynomial Calculus for Arithmetic Circuit Verification
multitope	(HDRA) The equivalence between opetopic sets and many-to-one polygraphs
muMALL	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points
N
N player games	(LICS) Rational Synthesis Under Imperfect Information
nanoCoP	(PAAR) Proof Search Optimizations for Non-clausal Connection Calculi
Nanofabricated Devices	(VEMDP) Formal Verification of Network-Based Biocomputation Circuits
narrowing	(WPTE) On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions
Nash equilibria	(SR) Compositional Game Theory
Nash equilibrium	(LICS) Rational Synthesis Under Imperfect Information (SR) Local Equilibria in Logic-Based Multi-Player Games
Natural deduction	(ITRS) Natural Deduction and Normalization Proofs for the Intersection Type Discipline (ThEdu) Natural Deduction Assistant (NaDeA) (PAAR) Efficient translation of sequent calculus proofs into natural deduction proofs (CL&C) On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains
Natural language	(UITP) Text-Orientated Formal Mathematics
natural language processing	(NLCS) Anti-Unification and Natural Language Processing (NLCS) OpenWordNet-PT: Taking Stock (MLP) Answering Cloze-style Software Questions Using Stack Overflow (MLP) Deep Learning On Code with an Unbounded Vocabulary
natural language understanding	(ICLP-DC) The Learning-Knowledge-Reasoning Paradigm For Natural Language Understanding and Question Answering (NLCS) OpenWordNet-PT: Taking Stock (ICLP) An ASP Methodology for Understanding Narratives about Stereotypical Activities
Natural mathematical language	(ThEdu) Towards intuitive reasoning in axiomatic geometry
natural proofs	(LCC) Feasibly constructive proofs of succinct weak circuit lower bounds
Natural-style Proofs	(SCSC) EA: Techniques for Natural-style Proofs in Elementary Analysis
Negation as failure	(ICLP) Cumulative Scoring-based Induction of Default Theories
Negation in Logic Programming	(ICLP) Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs
Negative translations	(LICS) Around Classical and Intuitionistic Linear Logics
neighbourhood semantics	(EICNCL) Toward intuitionistic non-normal modal logic and its calculi
neighbourhood singleton arc consistency	(RCRA) Partial (Neighbourhood) Singleton Arc Consistency for Constraint Satisfaction Problems
Nelson-Oppen	(IJCAR) Complexity of Combinations of Qualitative Constraint Satisfaction Problems
Nested	(VSTTE) Extending VIAP to Handle Array Programs
nested sequents	(TYDI) Nested sequents for modal logics and beyond
nested systems	(TYDI) Sequentialising nested systems (WiL) A semantical view of sequent based systems
Network Based Biocomputation	(VEMDP) Formal Verification of Network-Based Biocomputation Circuits
Network Intrusion Detection	(FCS) LISA: Predicting the Impact of DoS Attacks on Real-World Low Power IoT Systems
Network-free simulation	(VEMDP) Rule-Based Gillespie Simulation of Chemical Systems
networks of synchronized automata	(AVOCS) Using SMT engine to generate Symbolic Automata
neural network	(DS-FM) Formal verification of neural networks
neural networks	(PAAR) Dynamic Strategy Priority: Empower the strong and abandon the weak
Newman's lemma	(IWC) Critical pairs for Gray categories
next state relation	(IJCAR) A FOOLish Encoding of the Next State Relations of Imperative Programs
no-go theorem	(MSFP) Some No-Go Theorems for Distributive Laws (extended abstract)
Noise Reduction	(VEMDP) Molecular Filters for Noise Reduction
nominal rewriting	(UNIF) Rewriting with Generalized Nominal Unification
nominal terms	(FSCD) Fixed-Point Constraints for Nominal Equational Unification
nominal unification	(FSCD) Fixed-Point Constraints for Nominal Equational Unification (FSCD) Nominal Unification with Atom and Context Variables (UNIF) Rewriting with Generalized Nominal Unification
nominalizations	(NLCS) OpenWordNet-PT: Taking Stock
non-clausal theorem proving	(PAAR) Proof Search Optimizations for Non-clausal Connection Calculi
non-cnf	(SAT) Circuit-based Search Space Pruning in QBF
non-commutative	(Linearity/TLLA) On the Lambek Calculus with an Exchange Modality
non-denoting terms	(ARQNL) Labelled Calculi for QMLs with Non-Rigid and Non-Denoting Terms
Non-Deterministic Automata	(LICS) One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
non-deterministic mealy machine	(SYNT) Minimal Synthesis of String To String Functions From Examples
non-idempotency	(LICS) Every λ-Term is Meaningful for the Infinitary Relational Model
non-idempotent intersection types	(ITRS) Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus
Non-interference	(CSF) Inductive Invariants for Noninterference in Multi-agent Workflows
Non-interleaving semantics	(CAV) Quasi-Optimal Partial Order Reduction
Non-lawlike computability	(LICS) Computability Beyond Church-Turing via Choice Sequences
non-linear arithmetic	(SCSC) EA: Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT
Non-linear Real Arithmetic	(SCSC) RP: Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics
Non-monotonic Reasoning	(RCRA) Externally Supported Models for Efficient Computation of Paracoherent Answer Sets
non-normal modal logic	(EICNCL) Toward intuitionistic non-normal modal logic and its calculi
non-normal modal logics	(EICNCL) Proof theory for quantified monotone modal logics
non-rigid terms	(ARQNL) Labelled Calculi for QMLs with Non-Rigid and Non-Denoting Terms
Non-Termination Bugs	(CAV) Symbolic Liveness Analysis of Real-World Software
Non-termination Proving	(CAV) Syntax-Guided Termination Analysis
Non-wellfounded proofs	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points (CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs
non-zero sum games	(LICS) Rational Synthesis Under Imperfect Information
nondeterminism	(LPOP) A software system should be declarative except where it interacts with the real world (DCM) Generic Graph Semantics (LICS) Classical realizability as a classifier for nondeterminism
nonlinear integer arithmetic	(IJCAR) A Why3 framework for reflection proofs and its application to GMP's algorithms (SAT) Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
NonMonotonic Semantics	(ICLP) Declarative Algorithms in Datalog with Aggregates: user-friendly formal semantics conducive to performance and scalability
nonmonotonic term orders	(IJCAR) Superposition for Lambda-Free Higher-Order Logic
nonnegativity certificate	(PC) Optimization over the Boolean Hypercube via Sums of Nonnegative Circuit Polynomials
nontermination	(VSTTE) Loop Detection by Logically Constrained Term Rewriting
Normal Form	(PAAR) Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics
normal form bisimulation	(ITP) A Formal Equational Theory for Call-by-Push-Value
normal forms	(HDRA) Normal forms for planar connected string diagrams
normalisation	(FSCD) Strict Ideal Completions of the Lambda Calculus (TYDI) Two Unifying Structural Principles
Normalization	(ITRS) Natural Deduction and Normalization Proofs for the Intersection Type Discipline (HOR) Normalization and Taylor expansion of lambda-terms
norms	(VaVAS) Social Consequence Engines (Abstract)
Notation	(LFMTP) What Does This Notation Mean Anyway? BNF-style notation as it is actually used (Coq) Teaching Your Rooster to Crow in C
Notebooks	(F-IDE) A Notebook Format for the Holistic Design of Embedded Systems
novel applications domains	(SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
Nowhere dense graphs	(LICS) On the number of types in sparse graphs
Numerical optimization	(MLP) Difflog: Beyond Deductive Methods in Program Analysis
Numerical Program Analysis	(CAV) Fast Numerical Program Analysis with Reinforcement Learning
Nuprl	(WiL) On Expanding Standard Notions of Constructivity
Nuprl proof assistant	(LICS) Computability Beyond Church-Turing via Choice Sequences
nuxmv	(AVOCS) A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways
O
o-minimality	(MoRe) Stochastic o-minimal hybrid systems
OBDD	(PC) Branching Program Complexity of Canonical Search Problems and Proof Complexity of Formulas
Object Constraint Language (OCL)	(LPOP) Security Policies in Constraint Handling Rules
object-oriented	(FM) Object-Oriented Security Proofs
Object-oriented programs	(FM) A lightweight deadlock analysis technique of object-oriented programs
observational equivalence	(LICS) Probabilistic Böhm Trees and Probabilistic Separation (ITP) A Formal Equational Theory for Call-by-Push-Value (WPTE) Automating the Diagram Method to Prove Correctness of Program Transformations
OCaml library	(LFMTP) Abstract Representation of Binders in OCaml using the Bindlib Library
Ocra	(AVOCS) A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railways
odd-even network	(POS) Competitive Sorter-based Encoding of PB-Constraints into SAT
omega-automata	(SYNT) Reactive Synthesis from LTL Specification with Spot
omega-languages	(FM) A Weakness Measure for GR(1) Formulae (LICS) A Theory of Register Monitors
Omega-regular languages	(LICS) Automaton-Based Criteria for Membership in CTL
omega-regular objectives	(MoRe) Parameterized complexity of games with monotonically ordered omega-regular objectives (MoRe) Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives
OMT	(SMT) Puli - A Problem-Specific OMT Solver
Online Decomposition	(CAV) Fast Numerical Program Analysis with Reinforcement Learning
Online Social Networks	(FM) Timed Epistemic Knowledge Bases for Social Networks
ontologies	(IJCAR) FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics
Ontology	(ICLP-DC) Natural Language Generation From Ontologies
Ontology Languages	(PRUV) Leveraging Probabilistic Existential Rules for Adversarial Deduplication
Ontology Reasoning	(ICLP) Natural Language Generation From Ontologies: Application Paper
open games	(LICS) Compositional game theory (SR) Compositional Game Theory
open set lattice	(Domains13) Invited Talk: Topology and Domain Theory Interfaces
Open-WBO	(SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers
OpenFlow	(FM) SDN-Actors: Modeling and Verification of SDN Programs
OpenJDK	(F-IDE) Experience Report on Formally Verifying Parts of OpenJDK's API with KeY
OpenJML	(VSTTE) Practical Methods for Reasoning about Java 8's Functional Programming Features
OpenTheory	(LFMTP) Sharing a library between proof assistants: reaching out to the HOL family
Operad	(HDRA) Generalizations of the associative operad and convergent rewrite systems (Linearity/TLLA) Generalized generalized species of structure and resource modalities
Operating System Verification	(ITP) Program Verification in the Presence of Cached Address Translation
operational semantics	(FM) Operational Semantics of a Weak Memory Model with Channel Synchronization (FM) A wide-spectrum language for verification of programs on weak memory models (CSF) KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (Linearity/TLLA) The Bang Calculus and the Two Girard's Translations (LOLA) A more precise, more correct stack and register model for CompCert (WPTE) Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
Operational Termination	(WST) Well-founded models in proofs of termination
opetope	(HDRA) The equivalence between opetopic sets and many-to-one polygraphs
Optical Networks on Chip	(RCRA) Logic Programming approaches for routing fault-free and maximally-parallel Wavelength Routed Optical Networks on Chip (Application paper)
optimal propagation	(SAT) Approximately Propagation Complete and Conflict Propagating Constraint Encodings
Optimal Scheduling	(ICLP) Optimal Scheduling for Exposed Datapath Architectures with Buffered Processing Units by ASP
Optimal Upper Bound	(LICS) A Simple and Optimal Complementation Algorithm for Büchi Automata
Optimisation	(Overture) Design Space Exploration for Secure Building Control (RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network (RCRA) Greedy Randomized Search for Scalable Compilation of Quantum Circuits
optimization	(DS-FM) Formal verification of neural networks (CAV) Delta-Decision Procedures for Exists-Forall Problems over the Reals
Optimization heuristics	(MoRe) Multi-Scenario Uncertainty in Markov Decision Processes
Optimization Modulo Bit-Vectors	(SAT) Solving MaxSAT with Bit-Vector Optimization
optimization techniques	(PAAR) Proof Search Optimizations for Non-clausal Connection Calculi
optimizations	(ITP) A Formal Equational Theory for Call-by-Push-Value
OR causality	(LICS) Concurrency and Probability: Removing Confusion, Compositionally
oracle Turing machines	(LICS) Type-two polynomial-time and restricted lookahead.
Order enriched categories	(Domains13) Extending Stone Duality to Relations
order invariant definability	(LCC) Traversal-invariant definability and Logarithmic-space computation
order theory	(SR) Beyond admissibility: Dominance between chains of strategies
order-preserving embeddings	(MSFP) Everybody's Got To Be Somewhere
ordered completion	(IWC) Certified Ordered Completion
ordered objectives	(MoRe) Parameterized complexity of games with monotonically ordered omega-regular objectives
ordered structures	(HoTT/UF) Ordered Cubes
ordering	(UNIF) Unification based on generalized embedding
ordinal diagram system	(TERMGRAPH) On quasi ordinal diagram systems
Ordinary differential equation	(CAV) Monitoring CTMCs By Multi-Clock Timed Automata
ordinary differential equations	(FM) Vector Barrier Certificates and Comparison Systems
Origin	(LICS) Logics for Word Transductions with Synthesis
over-approximation	(FSCD) Completeness of Tree Automata Completion
overt set	(Domains13) T^\omega-representations of compact sets through dyadic subbases
Overture	(Overture) Integrating VDM-SL into the continuous delivery pipelines of cloud-based software (Overture) VDM at large: analysing the EMV Next Generation Kernel (Overture) Overture FMU: Export VDM-RT Models as Tool-Wrapper FMUs
P
Paracoherent Answer Sets	(RCRA) Externally Supported Models for Efficient Computation of Paracoherent Answer Sets
Paraconsistent logic	(ARQNL) Formalization of a Paraconsistent Infinite-Valued Logic
Parallel computation	(DCM) A Category Theoretic Interpretation of Gandy’s Principles for Mechanisms
parallel improvements	(WPTE) Optimizing Space of Parallel Processes
Parallel Processing	(POS) Tuning Parallel SAT Solvers
Parallel Zielonka's Algorithm	(PLR) An Efficient Zielonka's Algorithm for Parallel Parity Games
parallelism	(ICLP) MASP-Reduce: a proposal for distributed computation of stable models
parameter optimization	(POS) CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances
parameter-free axioms	(PC)
parameterised Boolean equation systems	(ARQNL) Evidence Extraction from Parameterised Boolean Equation Systems
Parameterised verification problem	(FM) View abstraction for systems with component identities
parameterized AC^0	(LICS) Tree depth, quantifier elimination, and quantifier rank (LICS) A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
Parameterized Algorithms	(SAT) Exploiting Treewidth for Projected Model Counting and its Limits
parameterized complexity	(SAT) QBF as an Alternative to Courcelle's Theorem
Parameterized Model Checking	(IJCAR) Cubicle-W: Parameterized Model Checking on Weak Memory
parameterized systems	(CAV) Eager Abstraction for Symbolic Model Checking
Parameterized verification	(CAV) Peregrine: A Tool for the Analysis of Population Protocols (HCVS) Declarative Parameterized Verification of Topology-sensitive Distributed Protocols
Parametricity	(LICS) A General Framework for Relational Parametricity (LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (Coq) What is the Foreign Function Interface of the Coq Programming Language? (ITP) Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes
parametrized systems	(FM) Formal Specification and Verification of Dynamic Parametrized Architectures
Parity Game	(CAV) Strix: Explicit Reactive Synthesis Strikes Back! (CAV) Attracting Tangles to Solve Parity Games
parity games	(PLR) An Efficient Zielonka's Algorithm for Parallel Parity Games (SYNT) Reactive Synthesis from LTL Specification with Spot (LICS) A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (LICS) A modal mu perspective on solving parity games in quasipolynomial time. (SR) Dependences in Strategy Logic (SR) Infinite-Duration Richman Bidding Games (SR) Solving Parity Games: Explicit vs Symbolic
parsing	(NLCS) OpenWordNet-PT: Taking Stock (VSTTE) A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars
Partial algorithms in Coq	(ITP) Proof Pearl: Constructive Extraction of Cycle Finding Algorithms
partial correctness	(WPTE) Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
Partial Evaluation	(ASPOCP) Partial Evaluation of Logic Programs in Vector Spaces (WST) Control-Flow Refinement via Partial Evaluation
Partial Functions	(ICLP) Functional ASP with Intensional Sets; Application to Gelfond-Zhang Agreggates
Partial models	(FM) Multi-Robot LTL Planning Under Uncertainty
partial order reduction	(CAV) Partial Order Aware Concurrency Sampling (CAV) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (FM) SDN-Actors: Modeling and Verification of SDN Programs
Partial-order reduction	(CAV) Quasi-Optimal Partial Order Reduction
path orderings	(WST) GPO: A Path Ordering for Graphs
pattern matching	(Isabelle) Lazy Algebraic Types in Isabelle/HOL
paycheck pronouns	(NLCS) Paychecks, Presupposition, and Dependent Types
PB constraints	(RCRA) Encoding PB Constraints into SAT via Binary Adders and BDDs -- Revisited
PDL	(LICS) Wreath Products of Distributive Forest Algebras
PDR	(SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses (SAT) Finding all Minimal Safe Inductive Sets
PDR-Z3	(WPTE) Verification of Ada Programs with AdaHorn
Peano arithmetic	(PARIS) On the Logical Complexity of Cyclic Arithmetic (CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs
Perfect masking	(CAV) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks
perfect samplers	(SAT) Fast Sampling of Perfectly Uniform Satisfying Assignments
permission inference	(CAV) Permission Inference for Array Programs
permission model	(CSF) A Permission-Dependent Type System for Secure Information Flow Analysis
Permissions	(ADSL) A Complete Proof System for Basic Symbolic Heaps with Permissions
Permutation problems	(RCRA) Algebraic Crossover Operators for Permutations
permutations	(Coq) Preliminary Report on the Yalla Library
Persistent places	(LICS) Concurrency and Probability: Removing Confusion, Compositionally
Petri nets	(LICS) Concurrency and Probability: Removing Confusion, Compositionally
PGA	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
phase saving	(POS) Local-Style Search in the Linear MaxSAT Algorithm: A Computational Study of Solution-Based Phase Saving
Phylostatic	(ICLP) Natural Language Generation From Ontologies: Application Paper
Phylotastic	(ICLP-DC) Natural Language Generation From Ontologies
pi calculus	(LICS) Eager Functions as Processes
pi-caclulus	(WiL) A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract)
Pi-calculus	(DCM) Pointing to Private Names (LICS) Quasi-Open Bisimilarity with Mismatch is Intuitionistic
Picat	(LPOP) A Picat-based XCSP Solver - from Parsing, Modeling, to SAT Encoding
Picture Series	(LearnAut) Learning Graph Weighted Models on Pictures
Planning	(ICLP-DC) Scalable Robotic Intra-Logistics with Answer Set Programming (VaVAS) Social Consequence Engines (Abstract) (RCRA) Greedy Randomized Search for Scalable Compilation of Quantum Circuits (ICLP) Phylotastic: An Experiment in Creating, Manipulating, and Evolving Phylogenetic Biology Workflows Using Logic Programming
Planning under uncertainty	(MoRe) Multiple Objectives and Cost Bounds in MDP
Plotkin's T	(Domains13) T^\omega-representations of compact sets through dyadic subbases
PMCFG	(NLCS) Automatic test suite generation for PMCFG grammars
pointer arithmetic	(ADSL) On the Complexity of Pointer Arithmetic in Separation Logic
pointfree topology	(LICS) Computable decision making on the reals and other spaces via partiality and nondeterminism
polarity	(NLCS) Automated Reasoning from Polarized Parse Trees
Policing function	(VaVAS) Policing Functions for Machine Learning Systems
policy language	(FCS) An Expressive, Flexible and Uniform Logical Formalism for Attribute-based Access Control
Policy Synthesis	(MoRe) Logically-Constrained Reinforcement Learning
polycategories	(HDRA) Merge-bicategories: towards semi-strictification of higher categories
polygraph	(FSCD) Coherence of Gray categories via rewriting (HDRA) The equivalence between opetopic sets and many-to-one polygraphs
polygraphs	(HDRA) Merge-bicategories: towards semi-strictification of higher categories
Polyhedra Domain Analysis	(CAV) Fast Numerical Program Analysis with Reinforcement Learning
Polymers	(VEMDP) Conservative approximations of polymers
polymorphism	(SMT) Alt-Ergo 2.2 (LICS) Impredicative Encodings of (Higher) Inductive Types
Polynomial Calculus	(SCSC) RP: A Practical Polynomial Calculus for Arithmetic Circuit Verification
Polynomial Factorization	(ITP) A Formalization of the LLL Basis Reduction Algorithm
polynomial functor	(LICS) Dialectica models of type theory
Polynomial functors	(LICS) What's in a game? A theory of game models (HoTT/UF) Algebraic models of dependent type theory
Polynomial hierarchy	(IJCAR) Focussing, MALL and the polynomial hierarchy
polynomial simulation	(PC) On Dual-Rail Based MaxSAT Solving
polynomial upper bounds	(PC) On Dual-Rail Based MaxSAT Solving
polynomial-time tractability	(LICS) A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
polytyptic programming	(ITP) Relational Parametricity and Quotient Preservation for Modular (Co)Datatypes
population protocols	(CAV) Peregrine: A Tool for the Analysis of Population Protocols
port graphs	(TERMGRAPH) Finding the Transitive Closure of Functional Dependencies using Strategic Port Graph Rewriting
Portfolio	(QBF) Portfolio-Based Algorithm Selection for Circuit QBFs
Portfolio Solver	(POS) Tuning Parallel SAT Solvers
Positive complexity	(LCC) A recursion-theoretic characterisation of the positive polynomial-time functions
Post Correspondence Problem	(ITP) Verification of PCP-Related Computational Reductions in Coq (LOLA) Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic
power-law	(SAT) Sharpness of the Satisfiability Threshold for Non-Uniform Random k-SAT
powerlocale	(Domains13) Applications of entailments: de Groot duality
precision medicine	(RCRA) Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction.
precondition inference	(ICLP) An iterative approach to precondition inference using constrained Horn clauses
predecessor function	(ITP) Efficient Mendler-Style Lambda-Encodings in Cedille
predicate	(ICLP) Constraint Answer Set Programming without Grounding
Predicate Abstraction	(FM) Deadlock Detection for Actor-based Coroutines
preference	(ICLP-DC) Translating P-log, LP^{MLN}, LPOD, and CR-Prolog2 into Standard Answer Set Programs (PRUV) Evidential Group Decision Making Model with Belief-Based Preferences (ICLP) Introspecting Preferences In Answer Set Programming
Preference Logic	(PRUV) A new logic for jointly representing hard and soft constraints
Preference Modeling	(PRUV) A Model-Theoretic View on Preferences in Declarative Specifications of Search Problems
Preferential logics	(IJCAR) A Resolution-Based Calculus for Preferential Logics (PRUV) Reasoning about exceptions in ontologies: from the lexicographic closure to the skeptical closure
prefix-constrained term rewriting	(FSCD) Confluence of Prefix-Constrained Rewrite Systems
premature convergence	(RCRA) An Enhanced Genetic Algorithm with the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
preprocessing	(PAAR) Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics (IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
presheaf models	(HoTT/UF) Internalizing Presheaf Semantics: Charting the Design Space
presheaf semantics	(LICS) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
Presheaves	(LICS) What's in a game? A theory of game models
presupposition	(NLCS) Paychecks, Presupposition, and Dependent Types
pretty printing	(Coq) Teaching Your Rooster to Crow in C
primary key	(IJCAR) Automated Reasoning about Key Sets
Prime Numbers	(LICS) The State Complexity of Alternating Automata
priorities	(WiL) A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract)
prism	(MSFP) Profunctor Optics and the Yoneda Lemma
Privacy	(FM) Timed Epistemic Knowledge Bases for Social Networks (CSF) Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting (CSF) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
Privacy by design	(VSTTE) Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
Privacy-type properties	(CAV) The DEEPSEC prover
proactive security	(CSF) Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks
probabilistic	(ITP) Verified Analysis of Random Binary Tree Structures
Probabilistic Algorithm	(IJCAR) A New Probabilistic Algorithm for Approximate Model Counting (PRUV) A New Probabilistic Algorithm for Approximate Model Counting
probabilistic bisimilarity	(CAV) Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains
probabilistic bisimilarity distance	(CAV) Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains
Probabilistic Boolean Program	(CAV) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks
Probabilistic computation	(LICS) Probabilistic stable functions on discrete cones are power series.
probabilistic CTL	(LICS) Riesz Modal Logic with Threshold Operators
probabilistic finite automata	(LICS) Distribution-based objectives for Markov Decision Processes
probabilistic games	(CAV) Reactive Control Improvisation
Probabilistic graphical models	(ICLP) Constraint-Based Inference in Probabilistic Logic Programs
Probabilistic Inductive Logic Programming	(ICLP) Improving Candidate Quality of Probabilistic Logic Models
probabilistic lambda-calculus	(LICS) Probabilistic Böhm Trees and Probabilistic Separation
Probabilistic Logic	(IJCAR) Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic
Probabilistic logic programming	(ICLP) Constraint-Based Inference in Probabilistic Logic Programs
Probabilistic model checking	(CAV) Sound Value Iteration (CAV) Safety-Aware Apprenticeship Learning (F-IDE) A Notebook Format for the Holistic Design of Embedded Systems (VaVAS) Probabilistic Model Checking for Autonomous Agent Strategy Synthesis - Extended Abstract (VaVAS) Towards a Hierarchical-Control Architecture for Distributed Autonomous Systems (Extended Abstract - Paper) (VaVAS) Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot
Probabilistic planning	(VaVAS) Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot
probabilistic powerdomains	(Domains13) Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming
Probabilistic programs	(CAV) Constraint-Based Synthesis of Coupling Proofs (WST) Inference of Linear Upper-Bounds on the Expected Cost by Solving Cost Relations (LICS) The concurrent game semantics of Probabilistic PCF
probabilistic reasoning	(ICLP-DC) Probabalistic Action Language pBC+ (ICLP) A Probabilistic Extension of Action Language BC+
Probabilistic rewriting	(FCS) Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols
Probabilistic Satisfiability	(IJCAR) Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic
Probabilistic State Space Exploration	(CAV) Partial Order Aware Concurrency Sampling
probabilistic systems	(LICS) Distribution-based objectives for Markov Decision Processes
Probabilistic Timed Automata	(ITP) MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)
probabilistic verification	(CAV) Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (CAV) Constraint-Based Synthesis of Coupling Proofs (LICS) Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
probability	(GS) Continuous probability distributions in concurrent games (ITP) Verified Tail Bounds for Randomized Programs
problem database	(IJCAR) Cops and CoCoWeb: Infrastructure for Confluence Tools
problem encodings and reformulations	(SAT) Constrained Image Generation Using Binarized Neural Networks with Decision Procedures
problem fingerprinting	(POS) A Problem Meta-Data Library for Research in SAT
procedural interpretation	(ICLP) Top-down and Bottom-up Evaluation Procedurally Integrated
process calculi	(TYDI) Truely Concurrent Processes in the Calculus of Structures
process calculus	(Linearity/TLLA) Taking Linear Logic Apart
product types	(ITRS) Intersection Subtyping with Constructors
profunctor	(LICS) Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs-- (MSFP) Profunctor Optics and the Yoneda Lemma
Program Analysis	(CAV) Quasi-Optimal Partial Order Reduction (FM) Variant Analysis with QL (LaSh) Decidable Linear Tree Constraints (LICS) Polynomial Invariants for Affine Programs (ICLP) Shape Neutral Analysis of Graph-based Data-structures (ICLP) Towards Incremental and Modular Context-sensitive Analysis
program completion	(ASPOCP) anthem: Transforming gringo Programs into First-Order Theories (Preliminary Report)
program correctness	(ASPOCP) anthem: Transforming gringo Programs into First-Order Theories (Preliminary Report)
Program Debugging	(VSTTE) Executable Counterexamples in Software Model Checking
Program Derivation	(REFINE) Programming Without Refinement
program extraction	(LICS) A functional interpretation with state (Domains13) Invited Talk: Scott Domains for Denotational Semantics and Program Extraction
Program invariant	(LICS) Polynomial Invariants for Affine Programs
Program Projection	(REFINE) Programming Without Refinement
program refinement	(LICS) ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
program semantics	(Domains13) Invited Talk: Scott Domains for Denotational Semantics and Program Extraction
program specialisation	(ICLP) An iterative approach to precondition inference using constrained Horn clauses
Program Synthesis	(CAV) Synthesis Modulo Theories (CAV) Syntax-Guided Termination Analysis (CAV) Constraint-Based Synthesis of Coupling Proofs (CAV) Syntax Guided Synthesis with Quantitative Syntactic Objectives (CAV) Learning Abstractions for Program Synthesis (SYNT) Programming by example: efficient, but not “helpful” (IJCAR) Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions
program transformation	(FSCD) Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems (VSTTE) Relational Equivalence Proofs Between Imperative and MapReduce Algorithms (WPTE) Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics (WPTE) Automating the Diagram Method to Prove Correctness of Program Transformations (WPTE) On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems
program transformations	(FSCD) Nominal Unification with Atom and Context Variables (LOLA) Experimenting with graded monads: certified grading-based program transformations
Program translation	(TERMGRAPH) Programming by Term Rewriting
Program Verification	(DS-FM) Analysis and Verification of Message Passing based Parallel Programs (CAV) Syntax-Guided Termination Analysis (CAV) Nagini: A Static Verifier for Python (CAV) Program Analysis is Harder than Verification: A Computability Perspective (CAV) Formally Verified Montgomery Multiplication (Isabelle) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses (IJCAR) Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle (IJCAR) A FOOLish Encoding of the Next State Relations of Imperative Programs (ITP) Program Verification in the Presence of Cached Address Translation (ITP) Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper) (VSTTE) Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications (VSTTE) A Tree-Based Approach to Data Flow Proofs (VSTTE) Verified Certificate Checking for Counting Votes (WPTE) Verification of Ada Programs with AdaHorn (WPTE) Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics (HCVS) Metaprogramming and symbolic execution for detecting runtime errors in Erlang programs (ICLP) Solving Horn Clauses on Inductive Data Types Without Induction
Programming by example	(SYNT) Programming by example: efficient, but not “helpful”
programming language semantics	(LICS) Computable decision making on the reals and other spaces via partiality and nondeterminism (LICS) Work Analysis with Resource-Aware Session Types
programming languages	(LICS) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
programming logic	(IJCAR) A Separation Logic with Data: Small Models and Automation
programming methodology	(ASPOCP) anthem: Transforming gringo Programs into First-Order Theories (Preliminary Report)
programming paradigm	(LPOP) A software system should be declarative except where it interacts with the real world
Programming-by-Example	(CAV) Learning Abstractions for Program Synthesis
progress measure	(LICS) A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games
Projected Model Counting	(SAT) Exploiting Treewidth for Projected Model Counting and its Limits
projective limit	(Domains13)
Projective plane	(WiL) On Expanding Standard Notions of Constructivity
Prolog	(VSTTE) TWAM: A Certifying Abstract Machine for Logic Programs (ICLP) Top-down and Bottom-up Evaluation Procedurally Integrated (ICLP) Towards Static Performance Guarantees for Programs with Run-time Checks
Prompt LTL	(SR) Quantifying Bounds in Strategy Logic
Proof	(CAV) Continuous formal verification of Amazon s2n (Vampire) Testing ATP folklore: a statistical analysis of Vampire proofs.
proof assistant	(ARQNL) An Outline for Simple Semi-automated Proof Assistants for First-order Modal Logics (ThEdu) Lucas Interpretation from Programmers’ Perspective (IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (UITP) Interfacing with a Prover using Focusing and Logic Programming
proof assistants	(FSCD) Cumulative Inductive Types in Coq (ITP) HOL Light QE (ITP) The Coinductive Formulation of Common Knowledge (ITP) Reification by Parametricity
proof automation	(ITP) ProofWatch: Watchlist Guidance for Large Theories in E
proof by reflection	(ITP) Reification by Parametricity
proof checker	(WST) TTT2 with Termination Templates for Teaching
Proof checking	(POS) Two flavors of DRAT (UITP) Text-Orientated Formal Mathematics
proof complexity	(CAV) The Proof Complexity of SMT Solvers (PC) Resolution with Counting: Different Moduli and Tree-Like Lower Bounds (PC) Resolution and the binary encoding of combinatorial principles (PC) Proof systems for #SAT based on restricted circuits (PC) Branching Program Complexity of Canonical Search Problems and Proof Complexity of Formulas (TYDI) Proof complexity of deep inference: a survey (TYDI) Two Unifying Structural Principles (PARIS) On the Logical Complexity of Cyclic Arithmetic (LCC) Feasibly constructive proofs of succinct weak circuit lower bounds (IJCAR) Extended Resolution Simulates DRAT (POS) Seeking Practical CDCL Insights from Theoretical SAT Benchmarks (SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
Proof compression	(IJCAR) A Tableaux Calculus for Reducing Proof Size (UITP) Partial Regularization of First-Order Resolution Proofs
proof engineering	(Coq) Procrastination, A proof engineering technique (ITP) Reification by Parametricity
Proof generation	(SMT) Proofs in conflict-driven theory combination
proof guidance	(ITP) ProofWatch: Watchlist Guidance for Large Theories in E
proof identity	(IJCAR) From Syntactic Proofs to Combinatorial Proofs
Proof Method Recommendation	(Isabelle) PaMpeR: A Proof Method Recommendation System for Isabelle/HOL
Proof Mining	(Isabelle) PaMpeR: A Proof Method Recommendation System for Isabelle/HOL
proof nets	(FSCD) Proof nets for bi-intuitionistic linear logic (LICS) Unification nets: canonical proof net quantifiers (Linearity/TLLA) The structure of non decomposable connectives of linear logic (Linearity/TLLA) Proof nets, coends and the Yoneda isomorphism
proof of literal	(ASPOCP) Syntactic Conditions for Antichain Property in Consistency Restoring Prolog
proof of univalence	(HoTT/UF) Internalizing Presheaf Semantics: Charting the Design Space
proof schema	(PARIS) Towards the Automatic Construction of Schematic Proofs
Proof search	(IJCAR) Focussing, MALL and the polynomial hierarchy (Coq) Proof Construction by Tactic Learning (ADSL) Cyclic Theorem Prover for Separation Logic by Magic Wand
proof semantics	(TYDI) Two Unifying Structural Principles
Proof System	(Isabelle) Substitutionless First-Order Logic: A Formal Soundness Proof
proof systems	(IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (EICNCL) Proof Translations in BI logic
proof terms	(FSCD) ProTeM: A Proof Term Manipulator (CL&C) Fast cut-elimination using proof terms: an empirical study
Proof theory	(TYDI) Nested sequents for modal logics and beyond (TYDI) Sequentialising nested systems (TYDI) An introduction to deep inference (TYDI) Two Unifying Structural Principles (PARIS) On the Logical Complexity of Cyclic Arithmetic (WiL) Decomposing labelled proof theory for intuitionistic modal logic (WiL) Non-well-founded proof system for Transitive Closure Logic (WiL) Towards a Playground for Logicians (WiL) A semantical view of sequent based systems (PAAR) Efficient translation of sequent calculus proofs into natural deduction proofs (IJCAR) Focussing, MALL and the polynomial hierarchy (IJCAR) A Logical Framework with Commutative and Non-Commutative Subexponentials (IJCAR) A Tableaux Calculus for Reducing Proof Size (CL&C) Some ideas on cut-elimination for cyclic arithmetic proofs (CL&C) Admissible tools in the kitchen of intuitionistic logic (EICNCL) Intuitionistic multi-agent subatomic natural deduction for belief and knowledge (ICLP) First-order answer set programming as constructive proof search
proof theory of modal logic	(ITP) Software Tool Support for Modular Reasoning in Modal Logics of Actions
Proof translations	(EICNCL) Proof Translations in BI logic
proof-as-program	(LICS) Classical realizability as a classifier for nondeterminism
Proof-checker	(ITP) CalcCheck: a Proof Checker for Teaching the “Logical Approach to Discrete Math”
Proof-Producing Compilation	(VSTTE) TWAM: A Certifying Abstract Machine for Logic Programs
proof-relevant	(ICLP-DC) Proof-relevant resolution for elaboration of programming languages
Proof-relevant logic	(ICLP) Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
proof-search	(PARIS) Local Validity for Circular Proofs in Linear Logic with Fixed Points
proof-theoretic semantics	(NLCS) Paychecks, Presupposition, and Dependent Types
proof-theoretical linear semantics	(ICLP) A New Proof-theoretical Linear Semantics for CHR
proofs	(FM) Object-Oriented Security Proofs
Proofs by reflection	(IJCAR) A Why3 framework for reflection proofs and its application to GMP's algorithms
proofs-as-programs	(LICS) A sequent calculus with dependent types for classical arithmetic
proofs-as-programs-as-morphisms	(CL&C) The “duality of computation” from a fibrational perspective
property directed reachability	(SMT) Discovering Universally Quantified Solutions for Constrained Horn Clauses
property falsification	(CAV) Inner and Outer Approximating Flowpipes for Delay Differential Equations
Property Specification Patterns	(DS-FM) Consistency Checking of Functional Requirements
property-based testing	(LFMTP) Property-Based Testing of Abstract Machines: an Experience Report
Propositional Dynamic Logic	(CAV) Propositional Dynamic Logic for Higher-Order Functional Programs (LICS) Wreath Products of Distributive Forest Algebras
propositional implicational intuitionistic logic	(RCRA) Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic
propositional logic	(ARQNL) Pseudo-Propositional Logic (IJCAR) Extended Resolution Simulates DRAT (SAT) Exploiting Treewidth for Projected Model Counting and its Limits (CSF) Guided design of attack trees: a system-based approach (CL&C) Admissible tools in the kitchen of intuitionistic logic (PRUV) A new logic for jointly representing hard and soft constraints
propositional model counting	(PC) Proof systems for #SAT based on restricted circuits
Propositional Resizing	(HoTT/UF) Cubical Assemblies and the Independence of the Propositional Resizing Axiom
PROPs	(LICS) Rewriting with Frobenius
Protocol Verification	(CAV) Model checking indistinguishability of randomized security protocols (CSF) An extensive formal analysis of multi-factor authentication protocols
protokernel	(AVOCS) Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base
prototyping	(SAT) PySAT: A Python Toolkit for Prototyping with SAT Oracles
prover	(IJCAR) Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
Prover IDE	(UITP) Isabelle/PIDE after 10 years of development
Prover Trident	(FM) Interlocking Design Automation using Prover Trident
proximity relation	(UNIF) Proximity-Based Generalization
Pseudo-Boolean	(POS) Competitive Sorter-based Encoding of PB-Constraints into SAT
Pseudo-Boolean Optimisation	(RCRA) Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network
Pseudo-Boolean Solving	(POS) Divide and Conquer: Towards Faster Pseudo-Boolean Solving (SAT) Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers (SAT) In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
PSPACE	(FSCD) A Unifying Framework for Type Inhabitation
Public Git Archive	(MLP) Splitting source code identifiers using Bidirectional LSTM Recurrent Neural Network
Pushdown systems with transductions	(CAV) Android Stack Systems
PVS	(FM) A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (ITP) Boosting the Reuse of Formal Specifications (ITP) Formalizing Ring Theory in PVS (Short Paper)
Python	(LPOP) Logic-based Methods for Software Engineers and Business People (SAT) PySAT: A Python Toolkit for Prototyping with SAT Oracles
Q
Q-resolution	(SAT) Polynomial-Time Validation of QCDCL Certificates
QBF	(CAV) Synthesis Of Asynchronous Reactive Programs From Temporal Specifications (IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (QBF) A Grounder From Second-Order Logic To QBF (QBF) Portfolio-Based Algorithm Selection for Circuit QBFs (QBF) Towards the Semantics of QBF Clauses (SAT) QBF as an Alternative to Courcelle's Theorem (SAT) Polynomial-Time Validation of QCDCL Certificates
QBF calculi	(SAT) Local Soundness for QBF Calculi
QDimacs	(QBF) A Grounder From Second-Order Logic To QBF
QRAT	(IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
Qualitative Reasoning	(ICLP) A Trajectory Calculus for Qualitative Spatial Reasoning Using Answer Set Programming
qualitative spatial reasoning	(WiL) About the unification type of topological logics over Euclidean spaces
qualitattive spatial reasoning	(UNIF) About the unification type of topological logics over Euclidean spaces
quantale relator	(LICS) Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
quantification	(QBF) Tractability results for structured quantified CNF-formulas via knowledge compilation
Quantified Bit-Vectors	(CAV) Solving Quantified Bit-Vectors using Invertibility Conditions
quantified boolean formula	(SAT) Circuit-based Search Space Pruning in QBF
Quantified Boolean Formulas	(CAV) Understanding and Extending Incremental Determinization for 2QBF (IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (SAT) Symmetries for QBF
Quantified Circuit	(QBF) Portfolio-Based Algorithm Selection for Circuit QBFs
quantified effects	(LOLA) Experimenting with graded monads: certified grading-based program transformations
quantified modal logic	(ARQNL) An Outline for Simple Semi-automated Proof Assistants for First-order Modal Logics
quantified modal logics	(ARQNL) Labelled Calculi for QMLs with Non-Rigid and Non-Denoting Terms (EICNCL) Proof theory for quantified monotone modal logics
quantified resolution asymmetric tautology	(IJCAR) QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
Quantifier