View on GitHub


Curated List of Research Focused Reading Materials & Videos for Learning about Programming Language Theory Research, Formal Methods and their application in some most active computer Science fields.

Programming Language Theory & Formal Methods - Resources

FORSYTE group pics Image Courtsey : Forsyte group

Formal methods are mathematical techniques that are used for design, verification and specifications of software and hardware problems. These are essentially a subset of Programming Language Theory research that are being used to study complex computer science problems.

Analysis by Formal Methods basically involves these steps :

  1. Formal Specification
  2. Formal Proofs
  3. Model Checking
  4. Abstraction

The formal proof development and model checking are primarily done using interactive theorem provers often called as proof Assistants. Abstraction is creating structurally sound relations between parts of models.

Here is my attempt to curate a list of useful reading materials, videos and tools accompanied by some upcoming challenges in the field.


  1. I have tried to make the content more focused on current research and industrial application. People looking for purely academic collection must refer Formal Methods in Education - Jeremy Avigad.

  2. The reader is expected to have some basic knowledge of Type Theory. A more academic insight can be found here learn-tt.


Books & Lectures

If you feel you need more theoretical insights, please refer Note above.




Proof Assistants

SAT/SMT/SMC solvers

SAT Solvers :

SMT Solvers :

SMC Solvers :

Hybrid Solvers

Proof Assitants have very strong implmentations of program logics. Sometimes it may not be tactically possible to carry out complex proofs only by using them. Therefore Current research combines this principle of strong logic based reasoning with powerful SMT and SMC solvers to ease the proof development. Some examples are here below :


Most of the projects are more or less development of the respective theorem provers or SAT/SMT/SMC/ solvers and hence can be looked up there. These are some of other projects actively developed.

Upcoming Challenges

Abstract Interpretation focused

This particularily deals with improving certain properties (like Parallelism & Concurrency) of existing programming languages. A lot can be easily looked up in regard to this since after all this is the sole most important reason to study PL theory. All the conferences listed up in here ACM SIGPLAN have majority of research papers on programming language development do check them out.



Any suggestions are welcome. Please do consider submitting a pull request if you feel like !!