PL&CS.Materials

Public Materials for PL&CS Research/Study

(Extremely) slowly updating …

Note1: All of those material’s link are public on internet. They are collected based my personal interests.

Note2: Some of them are picked from great Chinese language materials (described only in Chinese) for people studying in China.

Programming Languages (Research Oriented)

a. Basic Programming Language Theory

  • Formal Semantics: TODO
  • Program Logic: TODO

b. Program Verification (Based on Proof Assistant )

  • The DeepSpec project
  • Formal verification & basic PL theory based on proof assistant Coq:
  • Formal verification - theoretical view
  • Reading List: Compiler Verification (CompCert C compiler and its variants)
    • Original CompCert Compiler (without linking or concurrency):
    • **Language-Independent Linking (Difficult problem, difficult approach) ** :
      • [POPL’15] Compositional CompCert
    • Language-Independent Linking (Difficult problem, difficult approach):
      • [POPL’15] Deep Specifications and Certified Abstraction Layers
    • Same compiler linking (but lightweight proof)
      • [POPL’16] Lightweight verification of separate compilation
    • Language-Independent Linking: CompCertM
      • [POPL’20] CompCertM: CompCert with C-assembly linking and lightweight modular verification
      • Difficult problem, simpler approach
    • Supporting Concurrency: CASCompCert
      • [PLDI’19] Towards Certified Separate Compilation for Concurrent Programs
    • Verified Translation Validator:
      • [POPL’08] Formal verification of translation validators: a case study on instruction scheduling optimizations
      • [OOPSLA’19] Certified and efficient instruction scheduling: application to interlocked VLIW processors
      • [CPP’22] Formally verified superblock scheduling
  • Separation Logic - Basic
    • Software Foundations, Volume 6
  • Separation Logic - Tools

c. Concurrency Theory

TBD

d. Parallel Programming

  • TODO
  • Concurrency vs. Parallelism

e. Program Analysis

  • Static Analysis Foundations:
  • Undecidability of Program Analysis: See Computability section below
  • Context Free Language Reachability for Static Analysis:
    • Read this paper from [POPL’95] to learn about how some static analysis problem can be reduced to graph-reachability problem
    • [Slides] TODO
  • Static Analysis for Parallel Program

Theoretical Computer Science (Interests Oriented)

a. Computability

  • Recursion Theory (Basic Computability)
    • [Textbook] Computability: An introduction to recursive function theory
    • [Slides] TODO
  • Undecidable Problems
    • Why Program Analysis is Undecidable: TODO
    • Rice Theorem: TODO

b. Computational Complexity

c. Algorithm

Logic & Foundation of Mathematics

a. Logic

  • First-order Logic
    • [Textbook] TODO
    • [Great Slides] TODO
  • Modal Logic
    • [Textbook] TODO
    • [Great Slides] TODO

b. Set Theory

  • TODO

Computer System (Courses Oriented)

  • Operating System
    • Course MIT 6.S081 and Labs from it
    • Xv6 Reference Book from 6.S081may be a better textbook for beginner’s (than those famous books)
    • A Chinese Textbook: 上海交大软院的IPADS实验室实验室撰写的这本中文教材 《现代操作系统：原理与实现》 是计算机类中文教材中难得的写得较好的一本（个人阅读过大部分内容，认为不适合初学；但如果初学过一遍操作系统导论课程仍然觉得不知所云，可以解决很多的疑惑）
  • Computer Architecture: TODO

$\alpha$. Tools