CS2612-Programming-Languages-and-Compilers

SJTU | CS 2612, Programming Languages and Compilers, Fall 2023

course website

Download and Install coq

Reference Books

• Pierce, Benjamin, et. al. Software Foundation.
• Winskel, Glynn. The Formal Semantics of Programming Languages: An Introduction.
• Harper, Robert. Practical Foundations for Programming Languages
• Appel, Andrew W. Modern Compiler Implementation in C

Regex Test

• https://regex101.com/
• https://regexr.com/

Common Problem

• Project Complie: coq_makefile -f _CoqProject *.v -o Makefile

• Incorrect display of Chinese characters (Displayed in Unicode), you could transfer it to normal Chinese Character by some common tools like: http://www.msxindl.com/tools/unicode16.asp

Coq Reference

• https://zhuanlan.zhihu.com/p/54164515

• https://coq-zh.github.io/SF-zh/lf-current/Preface.html

• https://le.qun.ch/en/blog/coq/