GLOBAL TALK KEYWORD INDEX

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

# | |

#SAT | |

#SMT(BV) | |

#SMT(LA) | |

2 | |

2-CNF | |

A | |

A-infinity-(co)algebras | |

abductive reasoning | |

Abella | |

ABNF | |

Absolute Correctness | |

abstract interpretation | |

abstract recursion theory | |

abstract state machine | |

Abstract State Machines | |

Abstract syntax | |

abstract winning condition | |

Abstraction | |

abstraction learning | (LearnAut) |

abstraction refinement | |

abstraction-refinement | |

accumulated weight constraints | |

Ackermann's Lemma | |

ACL2 | |

action language | |

Active Objects | |

Actor | |

actors | |

Actual Cause | |

ACUI | |

Ada programming | |

adaptive | |

additive monad | |

adequate numeral system | (ITRS) |

adjoint logic | |

adjoint model | |

adjunction | |

Adjunctions | |

admissibility | |

admissible rules | |

affine term | |

Agda | |

agent policies | |

agent programming | |

agents | |

Aggregates | |

aggregations in logic programming | |

AI Safety | |

air traffic surveillance systems | |

Alarm ranking | |

Algebra | |

algebra in type theory | |

algebraic confluence | |

Algebraic crossover operators | |

algebraic effects | |

Algebraic evolutionary computation | |

algebraic extensions | |

Algebraic Geometry | |

algebraic proof systems | |

algebraic structures | |

algorithm | |

Algorithm selection | |

algorithm substitution attacks | |

algorithmic complexity | |

algorithms | |

all maximal clique partitions in a graph | |

allegories | |

alloy | |

Almost Full relations | |

Almost-sure winning | |

alpha-equivalence | |

Alternating Automata | |

Alternating time | |

Alternating-time Temporal Logic | |

AMBA AHB | |

anaphora | |

Android Applications | |

Android back stack | |

Android stack systems | |

Animation | |

annotation | |

answer set | |

answer set computation | |

Answer Set Programming | |

Answer Set Programming Extensions | |

Anti-unification | |

Apache Spark | |

Application | |

applicative bisimulation distance | |

applicative first-order logic | |

applicative functor | |

applicative simulation distance | |

applied lambda-calculus | |

Apprenticeship Learning | |

Approximable Mappings | |

approximate circuits | |

approximate counting | |

approximate equivalence checking | |

Approximate inference | |

approximate partial order reduction | |

Approximate synthesis | |

Approximation | |

Approximation Fixpoint Theory | |

approximation theorem | |

architecture | |

Arithmetic | |

arithmetic circuits | |

Armstrong relation | |

Array | |

Arrays | |

arrow | |

Artificial Intelligence | |

ASMETA | |

ASN.1 | |

ASP | |

ASP systems | |

ASPIDE | |

Assertions | |

Associative operad | |

assumptions refinement | |

Asynchronous | |

Asynchronous Games | |

Atom tracing | |

atom variables | |

Atomic flows | |

Atomic Formula | |

ATP | |

Attack patterns | |

attack trees | |

attacker knowledge | |

Attempto Controlled English | |

attribute-based access control | |

Authentication | |

auto-generated code | |

autocorrelation | |

automata | |

automata learning | |

Automata over infinite words | |

automata theory | |

Automata with counters | |

Automated Algebraic Reasonings | |

automated complexity analysis | |

Automated configuration | |

Automated digital control | |

automated guided vehicle routing | |

automated reasoning | |

automated reasonning | |

automated theorem proving | |

automated trading systems | |

Automated verification | |

automatic algorithm configuration | |

Automatic Program Verification | |

Automatic Proof checking | |

automatic verification | |

automation | |

Automaton State | |

automotive | |

Automotive case study | |

Autonomous | (VaVAS) |

Autonomous automotive | |

Autonomous Driving | |

Autonomous system | |

Autonomous vehicle | |

autonomous vehicles | |

avatar | |

avionics systems | |

Axiom Pinpointing | |

axiomatic domain theory | |

Axiomatic Method | |

axiomatization | |

axioms | |

B | |

B combinator | |

B+ trees | |

back-and-forth equivalences | |

backdoor | |

backdoors | |

Backtracking | |

Backus FP | |

Backward exploration · | |

backwards analysis | |

Bar inductive predicates | |

barcan formulas | |

Barendregt's Variable Convention | |

Barrier Certificates | |

Basis Reduction | |

Bayesian inference | |

Bayesian learning | |

Bayesian network | |

BayesianInference | |

BDD | |

Behavioural equivalence | |

Behavioural metrics | |

Belenios | |

Belief Function Theory | |

belief merging | |

Belief networks | |

benchmark | |

Benchmarking | |

beta reduction | |

Beth models | |

Betweenness Centrality | |

Bi-directional Grammars | |

bi-intuitionistic logic | |

bicategories | |

Bidding games | |

Biform theories | |

BiLSTM | |

Bimonad | |

binarized neural network | |

binarized neural networks | |

Binary Analysis | |

Binary Encoding | |

binary search tree | |

binder mobility | |

Binders | |

Binding operations | |

Bioinformatics | |

bisimulation | |

bit-blasting | |

Bit-vectors | |

Bitcoin | |

Bitvectors | |

black-box optimization | |

BLESS | |

Blockchain | |

blocked clauses | |

bobs-only | |

boolean algebra | |

Boolean Functional synthesis | |

Boolean games | |

Boolean polynomials | |

Boolean Satisfiability | |

Boolean-valued models | |

Boot code | |

bottom-up | |

Bounded | |

bounded arithmetic | |

Bounded expansion | |

Bounded Model Checking | |

bounded model-checking | |

bounded synthesis | |

bounds on leakage | |

Braidings | |

branching programs | |

broadcast communication | |

Brzozowski derivatives | |

Buchberger algorithm | |

Buchi Automaton | |

Bug Finding | |

bug finding tool | |

Bunched Implications Logic | |

Business Process Model | |

Böhm trees | |

Büchi Automaton | |

C | |

C code | |

C Programming Language | |

cache coherence protocols | |

Cached Address Translation | |

CakeML | |

calculational method | |

Calculational proof | |

calculus of structures | |

call by push value | |

call by value | |

call-by-name | |

call-by-need evaluation | |

call-by-push value | |

call-by-push-value | |

call-by-value | |

CAMUS | |

car assembly operations | |

Cardinality Constraint | |

cardinality encodings | |

Cartesian cubes | |

Cartesian Genetic Programming | |

Cartesian Monoids | |

cartesian-closed | |

Case study | |

Catalan numbers | |

categorial grammar | |

Categorical Logic | |

Categorical model | |

Categorical models | |

Categorical Quantum Mechanics | |

Categorical semantics | |

Categories of relations | |

categories with families | |

Categorification | |

category | |

category theory | |

Causal Dependency | |

causality preservation | |

Cautious Reasoning | |

ccg | |

CCSL | |

CDCL | |

cdcl-cuttingplanes | |

Cedille | |

CEGIS | |

Cellular automata | |

cellular cohomology | |

Centrality | |

Certificate checking | |

certificates | |

certification | |

certified code | |

Certified execution engine | |

certified software | |

Certifying Compilation | |

channel composition | |

Character-level Language Model | |

chat bot | |

chemical computation | |

Chemical Reaction Networks | |

Chinese monoids | |

Choice Logic | |

choice sequence | |

Choice sequences | |

choiceless polynomial time | |

Chronological Backtracking | |

Church's type theory | |

Church-Turing thesis | |

circuit | |

Circuit complexity | |

circuit lower bounds | |

circuit satisfiability | |

circular proofs | |

classical arithmetic | |

classical B | |

classical higher-order logic | |

classical linear logic | |

classical logic | |

classical realizability | |

Classical sequent calculus | |

Clause Learning | |

CLF | |

clocks | |

closed set | |

cluster algebra | |

clustering | |

CNF | |

CNF configuration | |

Co-Simulation | |

Coalgebra Modality | |

Coarse computability | |

Coarse-grained modeling | |

CoCoA and MathSAT | |

codatatypes | |

code generation | |

Code Generators | |

code review | |

code-generation | |

coends | |

Cognitive Modeling | |

cographs | |

coherence | |

coherence theorems | |

coherent presentations | |

coinduction | |

coinduction up-to | |

Coinductive Invariants | |

coinductive types | |

Combination | |

Combinatorial benchmarks | |

combinatorial proofs | |

combinatorial search algorithms | |

combinatoric | |

Combinatorics | |

combinators | |

combinatory logic | |

common knowledge | |

Common Language for Geometric Problems | |

Commonsense Reasoning | |

commutative monads | |

comonads | |

Comparator | |

comparator network | |

comparison systems | |

CompCert | |

Competition | |

compiler | |

compiler verification | |

Compilers | |

complementary approximate reachability | |

Complementation | |

complete abstract domains | |

complete lattices | |

Complete Segal Spaces | |

completeness | |

completion | |

complex analysis | |

Complexity | |

Complexity Analysis | |

complexity classes | |

complexity dichotomy | |

Complexity measures | |

Complexity Proving | |

complexity results | |

Complexity Theory | |

composition | |

compositional analysis of software systems | |

compositional model checking | |

compositional reasoning | |

Compositional verification | |

compositionality | |

Computability | |

computable metric space | |

computation and deduction | |

Computation Complexity | |

Computation Tree Logic | |

computational complexity | |

computational effects | |

Computational Hardness | |

computational model | |

Computational modeling | |

computational monads | |

Computational Reductions | |

computational soundness | |

Computational thinking | |

computational type theory | |

computer aided security proofs | |

Computer Algebra | |

computer-aided cryptography | |

concurrency | |

concurrency and distributed computation | |

Concurrency Testing | |

Concurrent datatypes | |

concurrent dictionaries | |

Concurrent games | |

Concurrent objects | |

Concurrent operation specification | |

Concurrent Process Calculi | |

concurrent program algebra | |

concurrent programs | |

Concurrent Separation Logic | |

Concurrent strategies | |

Condition Synchronization | |

Conditional Independence | |

Conditional logic | |

conditional rewriting | |

conditional term rewriting | |

conditional value at risk | |

Confidentiality | |

conflict-driven clause learning | |

conflict-driven search | |

confluence | |

Confluence Analysis | |

Confluence and Standardization | |

confluence competition | |

Confluence modulo | |

confluence tool | |

Confusion | |

Congruence | |

Connection-based proof-search | |

cons-free computation | |

Conservative approximation | |

Conservativity | |

consistency | |

Consistency Analysis | |

Consistency Checking | |

Consistency proofs | |

constant-time security | |

Constrained Horn Clauses | |

Constrained Optimization | |

constrained rewriting | |

Constraint Handling Rules | |

Constraint Handling Rules (CHR) | |

Constraint Language | |

Constraint Logic Programming | |

Constraint Logic Programming on Finite Domains | |

Constraint Modelling | |

constraint problem | |

Constraint programming | |

constraint satisfaction | |

Constraint Satisfaction Problem | |

constraint satisfaction problems | |

Constraint satisfaction processing | |

Constraint Solving | |

Constraint Systems | |

Constraint-based synthesis | |

Constraint-based verification | |

constraints | |

constraints solver | |

constructive | |

Constructive Decidability | |

constructive mathematics | |

Constructive Type Theory | |

Constructive View of Theories | |

constructivism | |

contact logics | |

context-free | |

Context-free Grammars | |

contextual equivalence | |

contextual fibrancy | |

contextuality | |

Continuation Semantics | |

Continuous computation | |

Continuous delivery | |

continuous systems | |

continuous validation | |

continuous valuation | |

Continuous-time Markov chain | |

contract-based verification | |

contractibility | |

Contraction | |

control | |

control flow | |

control improvisation | |

Control parameters | |

Control-Flow Refinment | |

Controlled Natural Language | |

Controlled Natural Languages | |

controller synthesis | |

controller system | |

conversion algorithm | |

convex polyhedra | |

Cooperative Scheduling | |

Coq | |

Coq library | |

Coq proof assistant | |

Core SAT | |

Corecursion | |

correctness | |

Correctness by extraction | |

correctness criteria | |

Correctness Enhancement | |

Correctness proof | |

Correctness proofs | |

Correspondence theory | |

Cost Analysis | |

Cost bounded reachability | |

Cost relations | |

counter-example | |

CounterExample Guided Inductive Synthesis | |

Counterexample-guided Algorithms | |

Counterexample-Guided Inductive Synthesis | |

counterexamples | |

countermodel construction | |

counting classes | |

Courcelle's Theorem | |

Covering Theory | |

CPS translation | |

CR-Prolog | |

CR-Prolog2 | |

Crafted benchmarks | |

Craig Interpolation | |

Crime tracing | |

critical complexity region | |

critical pair | |

critical software assurance | |

Critical Systems | |

CRN | |

CRN equivalence | |

cross-fertilization | |

cross-section property | |

crowds | |

cryptographic CNF instances | |

cryptographic constant-time | |

Cryptographic protocol | |

Cryptographic protocols | |

cryptographic schemes | |

Cryptographic software | |

Cryptography | |

CSP | |

CSP Solver | |

cubical sets | |

cubical type theory | |

Curry-Howard | |

Curry-Howard correspondence | |

Curry-Howard isomorphism | |

cut elimination | |

cut-elimination | |

Cut-elimination theorem | |

Cutting and Packing | |

cutting planes | |

Cyber Security | |

Cyber-Physical system | |

cyber-physical systems | |

Cybercrime | |

Cycle finding | |

Cyclic graphs | |

cyclic induction | |

cyclic lambda calculus | |

cyclic proof | |

Cyclic proofs | |

cyclic sharing | |

Cyclic term-graps | |

Cylindrical Algebraic Decomposition | |

D | |

D-optimaldesigns | |

Daniell-Kolmogorov theorem | |

data compression | |

Data Driven modelling | |

data flow | |

Data Races | |

Data words | |

Data-structures | |

database theory | |

Databases | |

Datalog | |

datatypes | |

de Groot duality | |

Deadlock | |

Deadlock Analysis | |

Deadlock Detection | |

deadlock-freedom | |

Decentralized planning | |

Decidability | |

decision | |

Decision making | |

Decision Model and Notation (DMN) | |

Decision Modeling | |

Decision Modelling | |

decision procedure | |

Decision Procedures | |

decisiveness | |

Declarative Algorithms | |

declarative programming | |

Declarative Prover | |

declassification | |

decoupled approach | |

decreasing diagrams | |

deduction | |

Deductive interactive program verification | |

Deductive program verification | |

Deductive programs verification | |

deductive verification | |

Dedukti | |

Deduplication | |

deep embedding | |

deep inference | |

Deep Learning | |

Deficiency | |

definability | |

Definable | |

definable while programs | |

delay differential equations | |

Delta-completeness | |

denotation | |

denotational model | |

denotational semantics | |

deontic logis | |

Dependant Types | |

dependence maps | |

Dependency | |

dependency graph | |

dependent choice | |

dependent product types | |

Dependent Refinement Types | |

dependent temporal effects | |

dependent type theory | |

dependent types | |

dependently typed programming | |

derivational complexity | |

derivationism | |

Deriving Reliable Programs | |

Description logic | |

description logics | |

descriptive complexity | |

design automation | |

design by contract | |

Design Space Exploration | |

destructors | |

determinacy | |

Deterministic Automata | |

Deterministic Parity Automaton | |

DFA | |

Diagrammatic Reasoning | |

dialectica category | |

Dialectica interpretation | |

diamond lemma | |

diffeological spaces | |

differential dynamic logic | |

differential equation axiomatization | |

Differential Equations | |

differential game logic | |

differential ghosts | |

Differential Linear Logic | |

differential programming | |

Digital libraries | |

Diller-Nahm variant | |

Diophantine equations | |

direct-manipulation interaction | |

directed complete | |

Discounted-sum determinization | |

Discounted-sum inclusion | |

discrete polymorphism | |

Discrete-Event | |

discrete-time linear system | |

Display calculi | |

display map category | |

distance bounding protocols | |

Distance fraud | |

Distance-bounding protocols | |

distribute consensus protocols | |

distributed autonomous systems | |

distributed computing | |

distributed concurrent systems | |

Distributed Protocols | |

distributed systems | |

Distribution based objectives | |

distributive laws | |

division | |

DLVSYSTEM srl | |

DMN | |

DNA algorithmic self-assembly | |

DNF | |

Dolev-Yao Attacker | |

domain | |

domain equation | |

domain specific languages | |

domain theory | |

domain-level strand displacement | |

domain-specific formal languages | |

Domain-specific languages | |

dominance | |

Double Description method | |

Double negation | |

Double-pushout graph transformation | |

Double-pushout rewriting | |

downward closures | |

DPRM Theorem | |

drat | |

DRAT proofs | |

DSL | |

dual-rail encoding | |

duality | |

dualized proof system | |

Dynamic analysis | |

Dynamic applications | |

Dynamic data structures | |

Dynamic domains | |

dynamic epistemic logic | |

Dynamic language | |

Dynamic Languages | |

Dynamic Logic | |

Dynamic nets | |

Dynamic Partial Order Reduction | |

Dynamic Programming | |

Dynamic Verification | |

Dynamical Systems | |

E | |

e-voting | |

EasyCrypt | |

Eckmann-Hilton morphism | |

Economic Reasoning | |

Economics | |

effectful bisimilarity | |

Effective translations | |

Efficiency | |

Efficient Attractor | |

efficient computation | |

Egraph | |

Eilenberg-Moore Category | |

elaboration | |

Eldarica | |

Electronic Voting | |

elementary linear logic | |

elementary semantics | |

ellipsoid method | |

embedded domain specific language | |

Embedded systems | |

Empirical evaluation | |

EMVCo | |

energy games | |

energy-efficient computing | |

engineering mathematics | |

enriched categories | |

enriched category theory | |

entailment check | |

entailment relation | |

Entitity Resolution | |

epistemic logic | |

Epistemic Logic Program Solvers | |

Epistemic Logic Programs | |

Epistemic Negations | |

epistemic specification | |

Epistemic Specifications | |

equality by abstraction over an interval | |

equational constraints | |

equational logic | |

equational rewriting | |

Equational theories | |

equational theory | |

Equilibrium Logic | |

Equivalence | |

equivalence relations | |

erasure | |

Erin | |

Erin Triples | |

Erlang | |

essential unification | |

essentially algebraic theories | |

Ethereum | |

Evaluable Functions | |

Evaluation | |

Event Calculus | |

Event structures | |

evidential verification | |

Evolution systems | |

exceptions | |

exchange | |

exchange rule | |

Executable Harnesses | |

Executable Specifications | |

execution time | |

exhaustive and randomized data generation | |

Existential Rules | |

expander graphs | |

expansion proofs | |

expected shortfall | |

Expected Utility | |

experimental analysis | |

Experiments | |

Expert Systems | |

explainable decision set | |

explanation | |

explanatory analysis | |

explicit induction reasoning | |

explicit substitution | |

Exposed Datapath Architectures | |

expressiveness | |

extended resolution | |

Extension | |

extensive categories | |

extensive category | |

extensive-form games | |

External calculi | |

extraction | |

F | |

factorization | |

fairness | |

Fairness objectives | |

false negative rate | |

false positive rate | |

Fan Theorem | |

Fault tolerance | |

feasibility of functionals | |

feature tree constraints | |

fermionic quantum computing | |

fibrancy of the function type | |

fibrant replacement | |

fibred category theory | |

field theory | |

Filter | |

filter models | |

Finite Automaton | |

Finite model generator | |

finite model property | |

finite model theory | |

finite multisets | |

Finite Semantics | |

finite sum types | |

finitely partitioned trees | |

finitization | |

Firmware | |

first order theories | |

First order transduction | |

first-order combinatorial proofs | |

First-order list function | |

first-order logic | |

first-order logic with inductive definitions | |

first-order logic with inductive predicates | |

First-order multiplicative linear logic | |

First-Order Syntactic Unification | |

First-order Theory | |

first-order theory of rewriting | |

First-order types | |

Fishbone diagram | |

Fix-points | |

fixed parameter complexity | |

fixed parameter tractable | |

Fixed Point Arithmetic | |

fixed point equations | |

fixed points | |

fixed-point algorithms for synthesis | |

fixed-point logic | |

Fixpoint Algorithms | |

fixpoint alternation | |

fixpoint logic | |

fixpoints | |

flattener | |

Floating Point Arithmetic | |

floating-point | |

floating-point analysis | |

floating-point optimization | |

floating-point round-off errors | |

flocking | |

Flow Analysis | |

flows and nowhere-zero flows | |

Fly-Automata | |

FMI | |

Focused Proof Systems | |

focused sequent calculus | |

focused sequent calculus for first-order modal logic | |

Focusing | |

Focussing | |

FOIL algorithm | |

FOL | |

Forest Algebra | |

Forest Algebras | |

Formal Analysis | |

formal aspects of program analysis | |

Formal Definition | |

formal languages and automata theory | |

Formal Library | |

Formal Metatheory | |

Formal Methods | |

formal methods for security | |

formal methods in practice | |

Formal Model | |

Formal proof | |

formal proofs | |

formal reasoning | |

Formal Semantics | |

formal specification | |

formal topology | |

formal verification | |

formal verification at runtime | |

Formalisation | |

formalization | |

FormalVerification | |

forward proof-search | |

four-valued logic | |

Frama-C | |

Frames | |

Free choice sequences | |

free modules | |

free monad | |

Free Variable | |

Frege systems | |

Freyd categories | |

Frobenius algebra | |

FSM | |

Full abstraction | |

Function algebras | |

Function classes | |

function package | |

function summaries | |

Functional Analysis | |

functional and relational specifications | |

functional dependency | |

Functional interpretation | |

Functional Mock-up Interface | |

functional programming | |

functor | |

functor algebra | |

functorial spans | |

fuzz | |

fuzzer | |

fuzzy generalization | |

Fuzzy logic | |

G | |

g-leakage | |

Game semantics | |

game theory | |

Games | |

games and logic | |

games played on finite graphs | |

Gandy | |

Gappa | |

garbled circuit | |

generalised operads | |

generalised species | |

Generalization of syntactic parse trees | |

Generalized Reactivity | |

Generic Binding Structures | |

generic proof assistant | |

Genetic algorithms | |

Geometric Automated Theorem Provers | |

geometric realization | |

Geometry | |

geometry of interaction | |

Gillespie algorithm | |

Girard's translations | |

global states | |

gluing | |

GNATProve | |

goal-directed evaluation | |

graded monads | |

Gradient Boosting on Decision Trees | |

Gradient descent | |

Gradual Typing | |

grammar | |

Grammar testing | |

Grammatical Framework | |

grammatical inference | |

graph | |

graph algorithms | |

Graph Analysis | |

Graph Drawing | |

graph encoding | |

Graph Generation | |

graph grammars | |

graph isomorphism | |

graph minor theorem | |

graph neural networks | |

Graph Queries | |

Graph Recognition | |

Graph Representation | |

graph rewriting | |

graph rewriting systems | |

graph theory | |

Graph transformation | |

Graph Views | |

Graph Weighted Models | |

graph-based characterization | |

Graphical reasoning | |

Gray categories | |

Gray category | |

greatest fixed point | |

Greedy Heuristics | |

Groebner bases | |

Grothendieck fibrations | |

Grothendieck quasi-topos | |

ground systems | |

ground theories | |

Grounding | |

Group decision | |

Groupoid | |

Gröbner Basis | |

Guard Condition | |

Guarded Recursion | |

Guillotine Constraint | |

H | |

Hadamard matrices | |

halting problem | |

Hamiltonian cycle | |

hammers | |

Handlers | |

handwriting | |

Handwritten Digit Recognition | |

handwritten mathematics | |

hardness of approximation | |

Hardware model | |

hardware verification | |

hardware-in-the-loop | |

Hardware/software interfaces | |

hash functions | |

Hashing-based Algorithm | |

Haskell | |

HCI | |

head variable | |

heaps | |

herbrand theorem | |

Herbrand's theorem | |

hereditarily definable sets | |

hereditary substitution | |

heuristic search | |

Heuristics | |

hidden tree Markov model | |

Hierarchical information | |

Hierarchical state machines | |

Hierarchy Theorem | |

higher categories | |

higher dimensional categories | |

Higher dimensional linear rewriting | |

higher groups | |

higher inductive type | |

higher inductive types | |

Higher order recursion schemes | |

higher-order | |

Higher-order abstract syntax (HOAS) | |

higher-order computability | |

higher-order logic | |

higher-order logic programming | |

higher-order modal logic | |

higher-order operads | |

higher-order programs | |

higher-order reasoning | |

higher-order recursion schemes | |

higher-order rewriting | |

higher-order term rewriting | |

higher-order unification | |

Higher-Ranked Polymorphism | |

Highly Assured Software | |

Hilbert's tenth problem | |

Hilbert-Gentzen thesis | |

HKDF | |

HMAC | |

HOL | |

HOL Light | |

homogeneous | |

homogeneous linear diophantine equations | |

homogeneous types | |

Homological algebra | |

Homomorphism | |

Homotopical algebra | |

Homotopy | |

homotopy type theory | |

Hopf Monad | |

Horn clause | |

Horn Clause Transformation | |

Horn clauses | |

Horn propositional satisfiability algorithm | |

howe's method | |

HW-SW interface | |

hybrid logic | |

Hybrid System | |

hybrid system simulators | |

hybrid systems | |

hydraulic oil pump | |

Hyper sequents | |

hypercube optimization | |

Hyperintensional Logic | |

hyperltl | |

hyperproperties | |

Hyperproperty Verification | |

Hypersequent calculus | |

hypersequents | |

I | |

ic3 | |

IDE | |

Idempontent | |

Idempotent quasigroups | |

identifier | |

Identity type | |

IEEE-754 | |

ILP | |

immunization | |

imperative | |

imperative calculi | |

Imperative languages | |

imperative programming | |

imperative programs | |

Imperfect information | |

Implementation and benchmarks for parity games | |

implicate generation | |

implicative algebras | |

implicit complexity | |

Implicit Hitting Set | |

Importance Splitting | |

impredicative encodings | |

impredicativity | |

inconsistency measures | |

inconsistency-tolerant reasoning | |

Inconsistent Requirements Explanation | |

increasing chains | |

Incremental | |

Incremental Analysis | |

Incremental Maintenance | |

Incremental SAT | |

Indexed types | |

Indistinguishability | |

induction | |

induction principle | |

induction reasoning | |

induction rules | (PC) |

inductive datatypes | |

Inductive Definitions | |

Inductive invariants | |

Inductive Logic Programming | |

Inductive predicates | |

inductive theorem prover | |

Inductive Theorem Proving | |

inductive types | |

inductive validity cores | |

inductive-inductive types | |

Industrial application | |

industrial case | |

industrial impact | |

inference | |

inference attacks | |

infinitary and cyclic systems | |

Infinitary Proofs | |

infinitary rewriting | |

Infinite computation | |

infinite descent | |

infinite duration | |

Infinite modalities | |

infinite-state systems | |

Infinite-valued logic | |

Infinitely nested Boolean structure | |

Infinity-Categories | |

Infinity-Presheaves | |

informal proofs | |

Information Disclosure Analysis | |

Information Extraction | |

information flow | |

information flow analysis | |

Information flow control | |

Injectivity | |

inner-approximations | |

innermost conditional narrowing | |

Insider threat | |

instantiation | |

Integer Arithmetic | |

Integer Transition Systems | |

integer weights | |

Integrated Development Environment | |

integrated verification | |

Integration | |

integrity | |

Intension | |

intensional computation | |

Intensional Logic | |

Intensional Sets | |

Intensional Type Theory | |

Intentional attack | |

intentions | |

interaction graphs | |

Interaction nets | |

Interactive system | |

interactive theorem prover | |

interactive theorem proving | |

interactive tool | |

Interface design | |

Interlocking | |

Intermediate Language for Verification | |

intermediate representations | |

internal and external calculi | |

Internal calculi | |

internal language | |

internal parametricity | |

Internet of Things | |

Interoperability | |

Interpolation | |

Interpretable Machine Learning | |

interprocedural analysis | |

Intersection Type Systems | |

intersection types | |

intersections | |

interval arithmetics | |

interval propagation | |

Intrinsic noise | |

intruder deduction problem | |

intuitionism | |

intuitionistic combinatorial proofs | |

intuitionistic linear logic | |

Intuitionistic logic | |

Intuitionistic logic of constant domains | |

Intuitionistic mathematics | |

Intuitionistic Modal Logic | |

intuitionistic propositional logic | |

Invariant Checking | |

Invariant Generation | |

Invariant Synthesis | |

Invariants | |

Inverse Reinforcement Learning | |

IRM-calc | |

irrelevance | |

Isabelle | |

Isabelle Proof Assistant | |

Isabelle/HOL | |

Isabelle/HOL Theorem Proving | |

Isabelle/jEdit | |

IsaSAT | |

Isomorphism type | |

isotopy | |

Iterated Boolean games | |

J | |

JASP | |

Java | |

Java byte-code | |

JDLV | |

jEdit | |

JML | |

Jordan Normal Form | |

Judgemental Interpretation | |

Jung-Tix problem | |

Jupyter | |

K | |

k-safety verification | |

Kachinuki order | |

Kakutani's fixed point theorem | |

KeY | |

key set | |

kleptography | |

Knapsack | |

knot theory | |

Knowledge Acquisition | |

Knowledge and belief | |

Knowledge based Reasoning | |

knowledge compilation | |

Knowledge Representation | |

Knowledge Representation and Reasoning | |

knowledge-based noninterference | |

Knuth-Bendix criterion | |

Koat | |

Kripke model | |

L | |

L-derivative | |

Labelled calculi | |

labelled calculus | |

labelled Markov chain | |

Labelled proof-systems | |

labelled sequent calculi | |

Labelled sequents | |

labelled systems | |

lambda calculi | |

lambda calculus | |

lambda calculus and combinatory logic | |

lambda prolog | |

lambda-calculus | |

lambda-encodings | |

lambda-free higher-order logic | |

lambda-prolog | |

lambda-tree syntax | |

lambek calculus | |

lams | |

language based security | |

Language inclusion | |

large libraries | |

Large set | |

large theories | |

large-scale reasoning | |

lattice | |

Lattice Basis Reduction | |

lattice traversal | |

lax homomorphism | |

laziness | |

lazy | |

lazy evaluation | |

lazy grounding | |

lazy self-composition | |

Lean proof assistant | |

learning | |

Learning from positive examples | |

learning transductions | |

Learning Weighted Automata | |

learning-based testing | (LearnAut) |

Least general generalization | |

Lemma learning | |

lens | |

Leo-III | |

Leveled sequents | |

LFSR | |

Likelihood weighting | |

Lina | |

linear algorithm | |

Linear Arithmetic | |

Linear categories | |

Linear Category | |

linear clauses | |

linear cliquewidth | |

Linear Constraints | |

linear distributivity | |

linear logic | |

Linear polygraphs | |

Linear Programming | |

Linear Temporal Logic | |

linear term | |

linear time hierarchy | |

Linear Transformations | |

Linear Tree Constraints | |

linear-feedback shift register | |

linear/non-linear logic | |

Linearity | |

linearizability | |

Linearization | |

Lipschitz maps | |

Lists | |

Literate programming | |

Liveness Analysis | |

LLVM | |

Local determinism | |

Local Theory Extensions | |

locale theory | |

Log analysis | |

logarithmic space computation | |

logic | |

logic for PTime | |

Logic for Teaching | |

Logic Meta-Programming | |

Logic of Here and There | |

Logic on Trees | |

logic program | |

logic programming | |

Logic Programming Applications | |

Logic Solvers | |

Logic Tools | |

Logic-based tools | |

Logical complexity | |

logical design | |

logical formalism | |

logical framework | |

Logical Frameworks | |

Logical models | |

logical paradoxes | |

logical predicates | |

Logical Regulatory Networks | |

Logical relations | |

logically constrained term rewriting systems | |

Logics for strategic reasoning | |

Logistics | |

LOGSPACE | |

LOIS | |

long-distance resolution | |

loop unrolling | |

loops | |

low-level language | |

Lower Bounds | |

LPMLN | |

LPOD | |

LTI systems | |

LTLf | |

lucas interpretation | |

Lukasiewicz Logics | |

M | |

MAC | |

machine checked proofs | |

Machine Ethics | |

Machine Learning | |

Machine Learning Systems | |

machine words | |

magic states | |

Magic wand | |

MANET | |

Maple | |

MapReduce | |

MapReduce framework | |

MARCO | |

Markov Decision Process | |

Markov decision processes | |

Markov processes | |

Martin-L\"{o}f type theory | |

Martin-Löf type theory | |

Mason's Marks | |

Master Theorem | |

matching representation | |

mathematical analysis | |

Mathematical Induction | |

Mathematical language | |

mathematical proof | |

mathematical proofs | |

Mathematics | |

Matita | |

Matrix Growth | |

Matrix Interpretation | |

Matrix semigroups | |

Maude | |

maximum realizability | |

Maximum Satisfiability | |

MaxSAT | |

MAXSAT application | |

MaxSAT resolution | |

MaxSAT solving | |

maxSMT | |

MC-SAT | |

MCMT | |

mealy machine | |

mean-payoff games | |

meaningless terms | |

Measure theory | |

mechanical reasoning | |

mechanised theorem proving | |

mechanized mathematics | |

mechanized meta-theory | |

Mechanized proofs | |

mechanized reasoning | |

Memoization | |

Memory | |

Memory consistency models | |

Memory Errors | |

memory isolation | |

memory model | |

message passing concurrency | |

Message Passing Interface | |

meta programming | |

meta-data library | |

Meta-Interpretive Learning | |

meta-programming | |

Meta-theory | |

Metamorphic Testing | |

Metareasoning | |

metatheory | |

Metric Semantics | |

Minimal models | |

Minimal unsatisfiability | |

Minimally Adequate Teacher | |

Minimally strongly connected digraph | |

Minimisation | |

Minsky machines | |

MIPS TLB | |

Mixed Arithmetic | |

Mixed Distributive Law | |

Mixed Integer Linear Programming | |

ML | |

MMSNP | |

Mobile robotics | |

modal fixpoint logic | |

modal logic | |

Modal Logics | |

modal mu | |

modal mu calculus | |

Modal type theory | |

modalities | |

Model Animation | |

model checking | |

Model Checking Games | |

model construction | |

Model Counting | |

Model Expansion | |

model finding | |

model generation | |

Model learning | |

Model quality | |

Model Revision | |

model sampling | |

model theory | |

Model transformations | |

model-based engineering | |

model-based testing | |

model-checking | |

Model-checking first-order logic | |

model-checking problems | |

Model-level uncertainty | |

Modeling | |

Modeling and Specification | |

Modelling Languages | |

modelling secure protocols | |

models | |

Models of computation | |

Modular Analysis | |

modular approach | |

Modular Arithmetic | |

Modular System | |

Modular Tensor Category | |

modules | |

Molecular computing | |

Molecular Filters | |

Molecular programming | |

monad | |

Monadic Second Order Logic | |

Monads | |

monitoring | |

monoid | |

monoid model | |

monoidal categories | |

monoidal category | |

Monoidal Coalgebra Modality | |

monotone | |

Monotone complexity | |

Monotone proofs | |

monotonicity | |

Montague semantics | |

Montgomery Multiplication | |

MPI | |

MSO | |

MSO on Infinite Words | |

MSO on omega-Words | |

MSO transduction | |

mu-calculus | |

mu-mutilde-calculus | |

Multi Factor | |

Multi Modal logic | |

Multi-agent models | |

Multi-agent Systems | |

Multi-agent workflows | |

Multi-clock timed automata | |

Multi-dimensional | |

Multi-graphs | |

multi-modelling | |

multi-objective optimization | |

Multi-objective synthesis | |

Multi-party computation | |

Multi-Pass Dynamic Programming | |

Multi-player games | |

Multi-Robot planning | |

Multi-valued Logic | |

multicategories | |

multiplayer games | |

multiple languages | |

multiplicative linear logic | |

Multiplier Verification | |

multitope | |

muMALL | |

N | |

N player games | |

nanoCoP | |

Nanofabricated Devices | |

narrowing | |

Nash equilibria | |

Nash equilibrium | |

Natural deduction | |

Natural language | |

natural language processing | |

natural language understanding | |

Natural mathematical language | |

natural proofs | |

Natural-style Proofs | |

Negation as failure | |

Negation in Logic Programming | |

Negative translations | |

neighbourhood semantics | |

neighbourhood singleton arc consistency | |

Nelson-Oppen | |

Nested | |

nested sequents | |

nested systems | |

Network Based Biocomputation | |

Network Intrusion Detection | |

Network-free simulation | |

networks of synchronized automata | |

neural network | |

neural networks | |

Newman's lemma | |

next state relation | |

no-go theorem | |

Noise Reduction | |

nominal rewriting | |

nominal terms | |

nominal unification | |

nominalizations | |

non-clausal theorem proving | |

non-cnf | |

non-commutative | |

non-denoting terms | |

Non-Deterministic Automata | |

non-deterministic mealy machine | |

non-idempotency | |

non-idempotent intersection types | |

Non-interference | |

Non-interleaving semantics | |

Non-lawlike computability | |

non-linear arithmetic | |

Non-linear Real Arithmetic | |

Non-monotonic Reasoning | |

non-normal modal logic | |

non-normal modal logics | |

non-rigid terms | |

Non-Termination Bugs | |

Non-termination Proving | |

Non-wellfounded proofs | |

non-zero sum games | |

nondeterminism | |

nonlinear integer arithmetic | |

NonMonotonic Semantics | |

nonmonotonic term orders | |

nonnegativity certificate | |

nontermination | |

Normal Form | |

normal form bisimulation | |

normal forms | |

normalisation | |

Normalization | |

norms | |

Notation | |

Notebooks | |

novel applications domains | |

Nowhere dense graphs | |

Numerical optimization | |

Numerical Program Analysis | |

Nuprl | |

Nuprl proof assistant | |

nuxmv | |

O | |

o-minimality | |

OBDD | |

Object Constraint Language (OCL) | |

object-oriented | |

Object-oriented programs | |

observational equivalence | |

OCaml library | |

Ocra | |

odd-even network | |

omega-automata | |

omega-languages | |

Omega-regular languages | |

omega-regular objectives | |

OMT | |

Online Decomposition | |

Online Social Networks | |

ontologies | |

Ontology | |

Ontology Languages | |

Ontology Reasoning | |

open games | |

open set lattice | |

Open-WBO | |

OpenFlow | |

OpenJDK | |

OpenJML | |

OpenTheory | |

Operad | |

Operating System Verification | |

operational semantics | |

Operational Termination | |

opetope | |

Optical Networks on Chip | |

optimal propagation | |

Optimal Scheduling | |

Optimal Upper Bound | |

Optimisation | |

optimization | |

Optimization heuristics | |

Optimization Modulo Bit-Vectors | |

optimization techniques | |

optimizations | |

OR causality | |

oracle Turing machines | |

Order enriched categories | |

order invariant definability | |

order theory | |

order-preserving embeddings | |

ordered completion | |

ordered objectives | |

ordered structures | |

ordering | |

ordinal diagram system | |

Ordinary differential equation | |

ordinary differential equations | |

Origin | |

over-approximation | |

overt set | |

Overture | |

P | |

Paracoherent Answer Sets | |

Paraconsistent logic | |

Parallel computation | |

parallel improvements | |

Parallel Processing | |

Parallel Zielonka's Algorithm | |

parallelism | |

parameter optimization | |

parameter-free axioms | (PC) |

parameterised Boolean equation systems | |

Parameterised verification problem | |

parameterized AC^0 | |

Parameterized Algorithms | |

parameterized complexity | |

Parameterized Model Checking | |

parameterized systems | |

Parameterized verification | |

Parametricity | |

parametrized systems | |

Parity Game | |

parity games | |

parsing | |

Partial algorithms in Coq | |

partial correctness | |

Partial Evaluation | |

Partial Functions | |

Partial models | |

partial order reduction | |

Partial-order reduction | |

path orderings | |

pattern matching | |

paycheck pronouns | |

PB constraints | |

PDL | |

PDR | |

PDR-Z3 | |

Peano arithmetic | |

Perfect masking | |

perfect samplers | |

permission inference | |

permission model | |

Permissions | |

Permutation problems | |

permutations | |

Persistent places | |

Petri nets | |

PGA | |

phase saving | |

Phylostatic | |

Phylotastic | |

pi calculus | |

pi-caclulus | |

Pi-calculus | |

Picat | |

Picture Series | |

Planning | |

Planning under uncertainty | |

Plotkin's T | |

PMCFG | |

pointer arithmetic | |

pointfree topology | |

polarity | |

Policing function | |

policy language | |

Policy Synthesis | |

polycategories | |

polygraph | |

polygraphs | |

Polyhedra Domain Analysis | |

Polymers | |

polymorphism | |

Polynomial Calculus | |

Polynomial Factorization | |

polynomial functor | |

Polynomial functors | |

Polynomial hierarchy | |

polynomial simulation | |

polynomial upper bounds | |

polynomial-time tractability | |

polytyptic programming | |

population protocols | |

port graphs | |

Portfolio | |

Portfolio Solver | |

Positive complexity | |

Post Correspondence Problem | |

power-law | |

powerlocale | |

precision medicine | |

precondition inference | |

predecessor function | |

predicate | |

Predicate Abstraction | |

preference | |

Preference Logic | |

Preference Modeling | |

Preferential logics | |

prefix-constrained term rewriting | |

premature convergence | |

preprocessing | |

presheaf models | |

presheaf semantics | |

Presheaves | |

presupposition | |

pretty printing | |

primary key | |

Prime Numbers | |

priorities | |

prism | |

Privacy | |

Privacy by design | |

Privacy-type properties | |

proactive security | |

probabilistic | |

Probabilistic Algorithm | |

probabilistic bisimilarity | |

probabilistic bisimilarity distance | |

Probabilistic Boolean Program | |

Probabilistic computation | |

probabilistic CTL | |

probabilistic finite automata | |

probabilistic games | |

Probabilistic graphical models | |

Probabilistic Inductive Logic Programming | |

probabilistic lambda-calculus | |

Probabilistic Logic | |

Probabilistic logic programming | |

Probabilistic model checking | |

Probabilistic planning | |

probabilistic powerdomains | |

Probabilistic programs | |

probabilistic reasoning | |

Probabilistic rewriting | |

Probabilistic Satisfiability | |

Probabilistic State Space Exploration | |

probabilistic systems | |

Probabilistic Timed Automata | |

probabilistic verification | |

probability | |

problem database | |

problem encodings and reformulations | |

problem fingerprinting | |

procedural interpretation | |

process calculi | |

process calculus | |

product types | |

profunctor | |

Program Analysis | |

program completion | |

program correctness | |

Program Debugging | |

Program Derivation | |

program extraction | |

Program invariant | |

Program Projection | |

program refinement | |

program semantics | |

program specialisation | |

Program Synthesis | |

program transformation | |

program transformations | |

Program translation | |

Program Verification | |

Programming by example | |

programming language semantics | |

programming languages | |

programming logic | |

programming methodology | |

programming paradigm | |

Programming-by-Example | |

progress measure | |

Projected Model Counting | |

projective limit | |

Projective plane | |

Prolog | |

Prompt LTL | |

Proof | |

proof assistant | |

proof assistants | |

proof automation | |

proof by reflection | |

proof checker | |

Proof checking | |

proof complexity | |

Proof compression | |

proof engineering | |

Proof generation | |

proof guidance | |

proof identity | |

Proof Method Recommendation | |

Proof Mining | |

proof nets | |

proof of literal | |

proof of univalence | |

proof schema | |

Proof search | |

proof semantics | |

Proof System | |

proof systems | |

proof terms | |

Proof theory | |

proof theory of modal logic | |

Proof translations | |

proof-as-program | |

Proof-checker | |

Proof-Producing Compilation | |

proof-relevant | |

Proof-relevant logic | |

proof-search | |

proof-theoretic semantics | |

proof-theoretical linear semantics | |

proofs | |

Proofs by reflection | |

proofs-as-programs | |

proofs-as-programs-as-morphisms | |

property directed reachability | |

property falsification | |

Property Specification Patterns | |

property-based testing | |

Propositional Dynamic Logic | |

propositional implicational intuitionistic logic | |

propositional logic | |

propositional model counting | |

Propositional Resizing | |

PROPs | |

Protocol Verification | |

protokernel | |

prototyping | |

prover | |

Prover IDE | |

Prover Trident | |

proximity relation | |

Pseudo-Boolean | |

Pseudo-Boolean Optimisation | |

Pseudo-Boolean Solving | |

PSPACE | |

Public Git Archive | |

Pushdown systems with transductions | |

PVS | |

Python | |

Q | |

Q-resolution | |

QBF | |

QBF calculi | |

QDimacs | |

QRAT | |

Qualitative Reasoning | |

qualitative spatial reasoning | |

qualitattive spatial reasoning | |

quantale relator | |

quantification | |

Quantified Bit-Vectors | |

quantified boolean formula | |

Quantified Boolean Formulas | |

Quantified Circuit | |

quantified effects | |

quantified modal logic | |

quantified modal logics | |

quantified resolution asymmetric tautology | |

Quantifier |