# Applications of logic in theoretical and practical Computer Science [closed]

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.

• Are you primarily interested in what I might call "non-classical" logics, i.e., logics other than classical 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". Commented Nov 12, 2017 at 18:09
• This paper - aptly titled "On the Unusual Effectiveness of Logic in Computer Science" - may be of interest. Commented Nov 12, 2017 at 18:31
• Formal theories can be treated as formal grammars (see en.wikipedia.org/wiki/Formal_grammar). Commented Nov 12, 2017 at 20:28
• This is not a research-level question, nor is it a research-level reference request. And in any case, much better answers can be expected from computer scientists than from mathematicians, so I would suggest to move over to cs.stackexchange.com. I will answer the question over there, but not here. Commented Nov 12, 2017 at 20:29
• @AndrejBauer I asked it on cs.stackexchange Commented Nov 12, 2017 at 21:07