CS 430/530: Formal Semantics
Spring 2025, Yale University
We will use the
Ed Discussion
forum for announcements and discussions. See the
Quick Start Guide
to learn how to use Ed Discussion.
Last modified: October 15, 2024. This page is still under major construction!
Course Information
Schedule
Lecture Notes
Assignments
Projects
Online Documentations
Local copy of
Software Foundations
with
source files
by
Benjamin C. Pierce
and many others.
Coq
(v8.4pl2)  
Reference Manual
(
pdf
),
Standard Library
,
FAQ
, and
Tutorial
(
pdf
),
Proof General
and its
FAQ
,
User Manual
(
PDF
), and other
documentation
.
Certified Programming with Dependent Types
by
Adam Chlipala
Coq'Art
home pages,
CoqWiki
, the
coq-club
mailing list, and other
Coq documentation
.
GNU
Online Docs,
including the complete
Emacs
manual.
Frequently-Asked Questions (FAQ) for
Emacs
(
windows
) and
Unix
.
The Standard ML
Basis Library
The
SML/NJ
documentations
including
user guide
,
CM
, and
more
.
Bob Harper's
Programming in Standard ML
Copyright (c) 2025,
Zhong Shao
, Dept. of
Computer Science
,
Yale University