Can anyone suggest theoretical and/or practical applications of logic (modal, dynamic, Lukasiewici etc.) in Computer Science (like Markov Chains for linear algebra), as well as some open-source books or papers from which I can study by self?. I know for example that $PDL$ (Propositional Dynamic Logic) is used in

formalizing correctness specifications and proving rigorously that those specifications are met by a particular program. Other activities fall into this category as well: determining the equivalence of programs, comparing the expressive power of various programming constructs, synthesizing programs from specifications, etc. (Harel, Kozen, Tyurin - Dynamic Logic)

However, such examples as the one above are too broad. I'd like to know more concrete, hands-on applications, if possible.

other thanclassical propositional and predicate logic? What about type theory? Type theory is heavily used in modern proof assistants, but I'm not sure if you consider that to be "logic". $\endgroup$