I'm a student of logic and I'm interested in looking at logic applications, of which I am told there are many, in computer science and allied areas. I've seen some applications. More specifically, I keep seeing little things about security protocols which use logical methods. I'd like to learn some more about this material, although I suspect it may require I obtain a knowledge of networks and cryptography which I currently lack (although hopefully not for long!). I have recently obtained Ryan and Schneider's textbook on Security Protocols.

Are there any other suggestions for reading and self-teaching in this and / or other areas in computer science which use logical techniques / formal methods? (I expect there are many; just looking to be pointed in a couple of amenable directions which are reasonable for someone who knows some pure logic.)


I really like the phrase, as well as the book, that logic is calculus of computation. It is kind of hard to find an area in computer science where logic is not used. I will just mention few areas where knowing logic comes in handy.

  1. Verification. Techniques of logic are heavily used in verification area. Specification of hardware and software systems is usually given as logical formulas. Depending on what properties are being checked, such systems are also modeled by appropriate logic (propositional, FOL, modal logics, linear logic, etc.). Methods like satisfiability and model checking are usually used to check whether a system meets its specification. Moreover, there is an area of decision procedures that tries to come up with efficient procedures for checking satisfiability of formulas in various logics (by most first order theories). In general, you might want to take a look at automated theorem proving.
  2. Programming languages. As pointed earlier, there is a deep connection between programming languages and logic. By Curry-Howard isomorphism, every functional program is isomorphic to some proof in constructive logic. Logic is also used for defining axiomatic semantics of programming languages; see Hoare logic. Prolog is a programming language based on a paradigm where computation is specified by logical formulas. Lambda calculus was first intended as a formal logical system aimed to laying foundations of mathematics, but turn out to be more useful as a programming language. It is now at the core of every functional programming language.
  3. Misc. You might also be interested in the way logic and computability interplay. What might be specially interesting to you is descriptive complexity. Logic is also getting more attention in computational biology. It is also used in AI for knowledge representation.

Hope this gives you some kind of a starting point.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.