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 |