resources for automated therom proving

Next semester I will be taking CSCI-UA 480 Special Topics: Principles of Programming Languages by Professor Thomas Wies.

This course will be important for me to take further steps in automated thereom proving.

Here are some resources Prof Wies introduced.

• A series of books for introduction of functional programming: Software Foundation Series
• Book written by Prof Wies' Team Automated Verification of Concurrent Search Structures

Here are some more video-type resource I found:

• Introduction to Functional Programming in OCaml (This course is archieved, but their video is on YouTube). YouTube Link
  • I also found the GitHub Repo of the hw, Textbook and Project, and Solution to the hw.

---

Upate on 2024-10-16 19:41:59 The class is cancelled and I am instead doing a undergraduate research with Professor Wies.

I will upload my solution to the book: The Formal Semantics of Programming Languages: An Introduction Book by Glynn Winskel. My Github Repo is here

Books

• About concrete algorithms, recommanded by Prof Wies
  • The Calculus of Computation: Decision Procedures with Applications to Verification Book by Aaron R. Bradley and Zohar Manna
  • Decision Procedures: An Algorithmic Point of View Book by Daniel Kroening and Ofer Strichman
• Resources Recommanded by a PhD at CMU
  • Types and Programming Languages Benjamin C. Pierce
  • Practical Foundations for Programming Languages (Second Edition) by Robert Harper.
  • Type Theory and Formal Proof An Introduction
  • Mathematical Logic and Computation

I talked with Prof. Zhan on possible ways to translate symbolic computation to formal proofs

• Metaprogramming in Lean 4
• Iscalc: An Interactive Symbolic Computation Framework (System Description)
• A Bi-Directional Extensible Interface Between Lean and Mathematica
• About Coq: Certified Programming with Dependent Types Adam Chlipala (chapter about definitional equality (Reasoning about Equality Proofs), and one chapter about reflection (Proof by Reflection))
• Reification by Parametricity
• I read Prof. Zhan's this paper, the reason why I contacted him

More sysmematic resources:

Thanks to Professor Wies, he shared this repo on about resources on Programming Language: Programming Language Class Notes & homework