teaching

EAC 2nd ed. cover
August 16, 2026

Compiler Terminology

One field of Computer Science is Optimizing Compilers. Starting with the first high-level programming language Fortran in 1954, the field has a long history, and understandably, its terminology has become overloaded (no longer the Fortran Franca days). Compiler students and even established researchers today often use the same terms for different meanings. Part of the confusion is that the original wording, while appropriate in the past, becomes misleading in modern compilers. This post gives the traditional definitions for common terms and their sources, intermixed with background context based on my teaching of an advanced compiler course at URCS.

In Engineering a Compiler by Keith Cooper and Linda Torczon, a standard compiler textbook, the section (§8.3) on Scope of Optimization gives the following definitions:

  • Local methods “operate over a single-basic block.” In a basic block, “statements are executed sequentially” and “if any statement executes, the entire block executes.”
  • Global methods “use an entire procedure as context.” A typical representation of a procedure is a Control Flow Graph (CFG). In between local and global are regions based on particular properties, e.g., a loop nest, an Extended Basic Block (cycle-free), or a dominator tree. Global methods are also called intraprocedural.
  • Interprocedural methods “consider scopes larger than a single procedure.” They are sometimes called whole-program methods.

I used the Cooper-Torczon book when I created the advanced compiler course at URCS in the early 2000s, right when the first edition was published, and taught it for years. The first technique to teach students was local value numbering, with the original example from the 1971 paper by John Cocke (’87 Turing awardee) and Frances Allen (’06 Turing awardee, first woman to receive the award) titled “A Catalogue of Optimizing Transformations” and used the example from the EAC book to progress from local value numbering to regional methods based on EBBs and dominators. Students liked the material. Chris Stewart, now a professor at OSU, conceived a new idea during a lecture; students in later years came to know it as the Stewart extension

A compiler finds properties of program code, i.e., properties that hold on all its executions. This is known as the meet-over-all-path solution. When we consider a cyclic CFG, the number of possible paths becomes infinite. This is the course transition to data flow analysis.

  • Data flow analysis was pioneered by Kam and Ullman (2020 Turing awardee). It is the foundation of iterative analysis used by almost all compilers. An analogy is solving a recursive equation in math. Think of an iterative solution as the way to find a fixed-point solution. The key questions are convergence, speed of convergence, and the uniqueness of the solution. Their 1977 paper was titled “Monotone Data Flow Analysis Frameworks” and gave the monotone and distributive conditions for iterative analysis. Their earlier paper named the technique “Global Data Flow Analysis.”
  • Def-use chains are what some people think when they say “data flow”. Def-use analysis may be local or global. The resulting graph was called def-use chains in compiler papers.

Modern compilers, starting with LLVM, have converged on the intermediate representation called static-single assignment (SSA). Cytron, Ferrante, Rosen, Wegman, and Zadeck published the breakthrough technique in POPL’89 and TOPLAS’91. SSA was a direct improvement of def-use chains. Def-use chains may be quadratic in size in the worst case, SSA is linear. More useful is that SSA’s phi-functions more directly encode control flow information and makes data flow analysis simpler and more effective.

The SSA paper authors did not implement the technique. Keith Cooper, Ken Kennedy and their students were the first to test it out in the Rice compiler (SSA co-inventor F. Kenneth Zadeck was a student of Ken’s, graduated in 1983). EAC, first edition in 2003, is the first compiler textbook that teaches SSA and SSA-based compiler optimization. At the time, people questioned whether it was too advanced for undergraduate students. Chris Lattner, then a graduate student, created LLVM IR based on SSA. I don’t think it is coincidence that his advisor, Vikram Adve, was a researcher scientist at Rice at the time when SSA was first implemented. LLVM is now the most widely used compiler in the world.

My favorite data flow analysis in the Cooper-Torczon book is partial redundancy elimination (PRE). The classic formulation uses four coupled data flow equations. One year when taking my course, Linxiang Xiang implemented SSA-based PRE in Ruby. It was a most impressive compiler project.

In early days of CS, a PhD thesis might be just a new data flow analysis technique. In those days, everyone knew data flow to be the iterative compiler analysis. Now, people may use the term for its literal meaning but create confusion because it conflicts with the usage in the past. This triggered a lively discussion at Friday systems meeting and an email followup. I agree with my colleague Michael Scott (I have his Programming Language Pragmatics book right next to EAC on my shelf) who said “Yes, it’s kinda confusing. But if you try to redefine the terms it’s going to be even more confusing.“

Evolution of the Compiler Course

A motto in compiler teaching is learning a compiler by building one. As an undergrad at PKU, I took the compiler course taught by Sun Jiasu (孙家驯，北大70本) in sophomore year and then compiler practice by Professor Ding the next semester, which had no lecture and just one assignment: implement a compiler for a Pascal-like language (nested procedures, static scoping). As an MS student at Michigan, I took Steve Carr’s course and wrote an optimizer using Rice’s compiler base code. This was why as a PhD student at Rice, I sat in on Keith Cooper’s course but did not take it officially. My buddy Vijay Pai (later a tenured professor at Purdue ECE) took the course with me, vowing to beat the CS compiler wizard in the compiler project — but he couldn’t.

At the turn of the millennium, Rochester and Rice were the two smallest (with about 12 faculty members each) in the top 20 CS programs in the National Academy rankings. Rice was a compiler powerhouse, with many courses in computer systems but maybe one in AI (which I didn’t take). Rochester was an AI department with courses in computer vision, natural-language processing, robotics etc but mainly just two in systems: computer systems and programming systems. The latter teaches both compilers and programming languages, forming the basis of Michael’s popular PLP book, still the most adopted textbook on the subject among top 30 CS departments. After joining Rochester in July 2000, I taught the programming systems course for several years and then created the advanced compiler course as the follow-up course. When I teach either one, I require students to implement a compiler.

For teaching, I wrote a compiler IR in a handful of Java classes and asked students to write compiler passes on this compact IR. A kindred soul was Chris Lattner, then a PhD student attending the first ACM SIGPLAN MSP workshop Trishul Chilimbi and I co-organized with PLDI in Berlin in 2002. He told me that he was implementing an object-oriented compact IR, too, in C++.

Early students and TAs included my first two students, Yutao Zhong (who has taught at George Mason in DC for many years) and Xipeng Shen (now directing the intelligent software center at Purdue). Bill Scherer (later research faculty at Rice) wrote a test suite for the teaching compiler. One program files a tax return (the 1040 form), and another draws the Mandelbrot set. The Scherer tests were used for many years to score student compilers by how much they reduce program instructions. When Ben Van Durme (now faculty at Johns Hopkins and research manager at Microsoft) took the course, he told me every day that he knew the exact way to remove two more instructions from one test program but it was too much pain for too little gain. The morning after the deadline, he ran into me, full of joy and pride, saying “I worked overnight and did it!”

Starting in the 1980s, GCC has been the foundation of open-source software. It was a real compiler but too complex for classroom use. In 2005, GCC 4.0 adopted a compact IR called GIMPLE. I invited its API designer, Diego Novillo, to visit Rochester (from Toronto) to give a guest lecture. Shortly after, I gave students the option and preparation to complete the compiler project in GCC, which at the time meant adding their code and compiling it alongside the other two million lines of source code. Tongxin Bai, then a PhD student, wrote GCC passes and Linux kernel modules (after taking the OS course from Sandhya Dwarkadas) as routine, had so much fun, and made money from his Google internship, he didn’t think about publishing and graduating. John Pershing (featured in the 2025 newsletter) was part of a group of undergrads who chose the GCC option for the compiler project and made the compiler work. As LLVM became widely adopted, it also became an option for the compiler project. Here is a project assignment from Rahman Lavaee in 2016. One year later, Dong Chen changed the two options to LLVM and Rust.

Xipeng Shen came to Rochester in 2001 as an AI student and switched to become my student after taking the compiler course. When he graduated in 2006, he knew more about computer systems than all AI professors and more about machine learning than all systems professors. His first job was at William and Mary where he taught two courses: compilers and AI. Many of his students have become professors. When I taught CS 258 in 2023, a student showed me the compiler course slides he found online by Yufei Ding, then a professor at UC Santa Barbara and now at UCSD. Some of the material had come full circle, after starting its life years ago right here in Rochester.

April 27, 2026

Miss Ratio Monotonicity and Convexity (Part 1)

Caches are dynamically managed local memories. Their dynamic behavior can either improve performance or, in some cases, become detrimental and counterproductive. Monotonicity and convexity are two properties are most commonly used to determine whether a cache design is well‑behaved and provides predictable performance. This is the first of a series blog posts on these properties.

Miss Ratio Monotonicity

Informally:

  • If you increase the cache size, the miss ratio never increases.
  • In other words, the miss ratio is a non‑increasing function of cache size.

Formally:
Let mr(c) be the miss ratio for a cache of size c (measured in blocks). Then for c_1 < c_2, we have mr(c_1) \ge mr(c_2).

Not all caches behave this way. If a cache algorithm is not monotonic, increasing cache size could sometimes increase misses, which is counterintuitive and undesirable. This is known as the Belady’s anomaly.

Stack Algorithms and the Inclusion Property

A caching algorithm has the inclusion property (or is a stack algorithm) if:

For any memory address reference sequence and at any time, the set of blocks in a cache of size c is a subset of the set in a cache of size c+1. Cache contents are inclusive across sizes. A block present in the smaller cache is always present in any larger cache. Therefore, the miss ratio of any stack algorithm is guaranteed non-increasing when increasing the cache size.

Mattson et al. Presented the stack property as the sufficient condition for one-pass evaluation of a caching algorithm. The Stack Simulation maintains the content of all cache sizes at each moment using a stack. At each access, the stack distance is the position of the stack where the accessed data is found. The stack distance fully determines whether the data access is a cache hit or miss.

After stack simulation, the hit or miss count of any cache size can be determined from the stack distances without re‑running the trace. Hence, the paper is titled Evaluation techniques for storage hierarchies.

The classic paper in 1970 established formally that the stack property is a sufficient condition for monotonic miss ratios, and the practical solution of one-pass evaluation. This classic work has been extended later in several ways.

LRU caches are the most important and commonly studied. For example, program locality analysis usually assumes LRU caches. The LRU stack distance shows the “closeness” of data reuse and is often abbreviated as the reuse distance. Stack simulation is too slow for large traces. Much faster algorithms have been developed. See a later blog devoted to studies of reuse distance.

Caching techniques that guarantee monotonic miss ratios:

  • Mattson et al. IBM 1970: LRU, OPT, MRU, LFU, and RR (statistically equivalent to RAND)
    • OPT is optimal for all cache sizes, while the technique for a single cache size is called Belady or MIN
  • Gu and Ding, ISMM 2011: LRU-MRU, used for collaborative caching with binary hints, i.e., the evict-me bit.
  • Gu and Ding, ISMM 2012: priority hints, Priority LRU, and non-uniform inclusion.

The term “stack distance” is often used without specifying which type. All stack algorithms above have their stack distance.

Caching techniques that are not guaranteed to have monotonic miss ratios:

  • Belady, CACM 1969: FIFO
  • Mattson et al. IBM 1970: RAND

As explained in Mattson et al., non-monotonic miss ratios may happen if caching priorities depend on the capacity of the cache and differ from one capacity to another, for example, priorities depending on the frequency of reference to pages after their entering the cache. Another example is when priorities depend on total time spent in the cache.

Summary

Miss ratio monotonicity means larger cache → same or lower miss ratio
Inclusion property ensures miss ratio monotonicity and allows for single-pass evaluation, i.e., you can compute miss ratio curve (MRC) for all cache sizes from one trace run.

March 21, 2026

Software Design and AI-assisted Development Course in Fall 2026

Announced to undergraduate students in an email on March 18, 2026:

Updated for Fall’26

CSC253 Software Design and AI-assisted Development

Software design is a critical discipline because modern software systems are too complex for any single individual to fully comprehend, yet they must be designed to avoid causing harm to the people they serve. This course focuses on the collaborative construction of software by teams. The curriculum covers:

  1. Design Principles and Practices: Information hiding, Parnas module and module decomposition, prototyping and extension, work assignments, team organization, iterative development, and documentation.
  2. Safe Programming in Rust: Generics and traits, ownership and borrowing rules, safe pointers, modules, and design patterns.
  3. AI Assistance: automated code and test generation, specialization, and coordination by coding agents.
  4. Ethical Principles: Fairness and human fallibility.

Assignments emphasize teamwork in software design and development. Students enrolled in CSC 453 are also required to learn Rust meta-programming.

Prerequisites:

  • CSC 172 (Data Structures and Algorithms) or equivalent for CSC 253.
  • CSC 172 and CSC 252 (Computer Organization) or equivalent for CSC 453.

Rust-related industry news:

Example uses:

  • A simple to-do list that runs entirely in a browser, written in either C or Rust using WASM SQLite. The following table compares the two choices. The complete code and commands are generated by DeepSeek (AI) here: https://chat.deepseek.com/share/wkgbopveuwb8cp1xsh
November 7, 2025

CSC 579 Logic Foundation and Machine-Checked Proofs

CSC 579 Spring 2026
(R 9:40am to 10:55 Wegmans 1005)

The language of intelligence is logic. The course teaches proof systems, with a focus on Coq. You will learn to use Coq to formalize logic, which is the fundamental language of rational thought and problem-solving, and construct sound and verifiable proofs. A similar system, Lean 4, was used by generative AI, Alpha Proof, to solve Olympiad-level math problems. By learning the fundamentals of modern proof systems, you acquire a complete foundation for logical thinking and the knowledge and skill to use or build automated reasoning systems.

Pre-requisites: Students enrolling in the course are expected to have advanced knowledge in either programming languages (CSC 253, 254 or 255), math, or logic.

Syllabus

  • The Need for Training Thought: The Values of Thought. Tendencies Needing Constant Regulation.  Regulation Transforms Inference into Proof.
  • Type Systems.  Operational Semantics. Progress. Type Preservation. Type Soundness.
  • Functional Programming in Coq: Data and Functions.  Proof by Simplification, Rewriting and Case Analysis.
  • Proof by Induction. Proofs Within Proofs.  Formal vs. Informal Proof.
  • Lists, Options, Partial Maps.
  • Basic Tactics: apply, apply with, injection, discriminate, unfold, destruct.
  • Logic in Coq. Logical Connectives: Conjunction, Disjunction, Falsehood and Negation, Truth, Logical Equivalence, Logical Equivalence, Existential Quantification.  Programming with Propositions. Applying Theorems to Arguments. Coq vs. Set Theory: Functional Extensionality, Propositions vs. Booleans, Classical vs. Constructive Logic.
  • Inductively Defined Propositions. Induction Principles for Propositions.  Induction Over an Inductively Defined Set and an Inductively Defined Proposition.
  • The Curry-Howard Correspondence. Natural Deduction. Typed Lambda Calculus. Proof Scripts. Quantifiers, Implications, Functions. Logical Connectives as Inductive Types.

Textbooks

Related Industry News

February 16, 2025

CSC 253 Collaborative Software Design Rate My Professor Chen Ding Fall 2024

Anonymous inputs were collected by the university before the final exam. 17 out of 24 students (71%) submitted the evaluation.The overall Instructor Rating is 4.53, and the overall Course Rating 4.44.

Two anonymous comments:

  • Professor Ding is a great professor and a strong proponent of Rust. Taking his class has introduced me to many benefits of Rust and broadened my horizon on collaborative programming, software design, and software testing. I believe acquiring these knowledge is beneficial for me and my teammates (it goes both ways) on the long run.
  • The final DVCS group project workload is very imbalanced and hard to control. Some group members even disappeared during the last half of the project.


Related posts:

September 4, 2024

CSC 252 Computer Organization Rate My Professor Chen Ding Spring 2024

This is a course required for the Bachelor of Science degree in Computer Science at the University of Rochester. A graduate must understand in depth the underlying physical reality which the virtual world including AI is built and depends on, i.e. the fundamentals of modern computer organization, including software and hardware interfaces, assembly language and C programming, memory hierarchy and program optimization, parallelism and operating systems. The textbooks are listed here.

There are two aspects for such a course in an elite research department like mine. First, the teaching focuses on fundamentals and goes in depth, which sets a high standard but this requirement is necessary for students to learn advanced subject courses later. Second, the material is updated often and part of it even experimental. In prior semesters, my colleagues Prof. John Criswell has emphasized on assembly and operating systems, Prof. Yuhao Zhu on gates and circuits, and Prof. Sree Pai on automatic (bit operation) correctness checking. My main change is the ISA.

RISC-V Instead of x86

Instruction Set Architecture (ISA) is essential in a BS CS degree and must be learned in this course which may be most hated material by a good number of students especially who have no prior knowledge of computer hardware. In my ancient PKU years, I learned Zilog Z80 (a microcontroller) and taught MIPS (classic RISC) and x86 (Intel/AMD) last time in this course in 2012. For the 2024 course, I evaluated Arm (Apple silicons) and the newest RISC-V. RISC-V is “open-source hardware” which means free for anyone to use. The course has the room to teach just one ISA; otherwise students will rebel.

I had a year to prepare for the course and tested this idea first before deciding on this significant change — This year’s students were the first (in Rochester) to learn RISC-V.

  • My NSF project with RIT has synthesized a RISC-V processor (papers here and here). I consulted my RIT collaborators who told me “x86 is too complex”, Arm is better but has “a lot of corner cases”, and for RISC-V, “I like it enough.” I learned about RISC-V over the years from computer architects to know the ISA is a good design, e.g., the first time in ASPLOS PC in 2019, but the RIT feedback made me think that the ISA is practical and learnable. The next question is whether it is teachable in a required undergrad class.
  • I purchased five or six single-board computers in both Arm and RISC-V and have them installed. Department staff Ian Ward installed Linux on Lichee-Pi 4A which has a quad-core processor, a GPU, and 8GB RAM for $130. The Arm processor (Raspberry Pi 4A) is weaker and does not run Linux.
  • My graduate TA Yifan Zhu (SchrodingerZhu on GitHub) installed the complete tool chain to compile and run RISC-V programs (in QEMU) on undergrad server (Intel) machines.
  • I found the 2024 textbook on RISC-V as recommended by the RISC-V foundation. The book reads well and covers the core knowledge: data representation, binary file and assembly, registers, data movement and control flow, application binary interface (ABI), all in 100 pages.

Here is the result. I summerized four changes in the following question (I created) in the Course Evaluation. Here are the question and the 15 responses:

RISC-V is newer and better designed, first with a core and then a series of extensions. The book covers RV32I, the core ISA. It is challenging to learn but learnable, unlike x86 which is too unwieldy, but it is 100 pages of material. Many students read the book and learned. They crossed a threshold of knowing the complete core, which they cannot do from learning x86.

Reading Books instead of Studying for Exams

At last semester’s CS Undergrad Town Hall where most CS faculty sat to listen to students’ feedback. One is that the department changes instructors of a course, and the exams are completely different from past years. I responded that a course teaches a subject, not a subject taught in a particular way and definitely not just exams. Exams are not the goal of learning or teaching, they are the feedback for both students and their teacher.

For this course, Prof. Zhu has made available past exams, problem sets, and their solutions (which I linked to in my course page). One can learn by studying these but shouldn’t use them as the primary source. Instead, students should learn by reading the textbooks. An important use of my lectures is to motivate students to read, show organization so they have mental map going in, and explain tricky/difficult examples and parts. When I find students don’t read textbooks, I use the lecture to read the book with them. My goal is for students to read the book and read it multiple times. The RISC-V book has the full content, updated, and readily accessible online.

The next and last 25 pages of the RISC-V book covers system-level programming (not covered in the course) but reading them (if/when they need to) would be a breeze once a student reads the first 100 pages.

In-person instead of Off-line Grading

The class has 64 students. 89 students registered, 21 dropped, and 5 withdrawn. Multiple students told me that they liked the course but felt not sufficiently prepared and will take the course next semester.

I myself cannot give every student the time and attention they deserve. There is no self deception/illusion/delusion here. I hired seven undergrad TAs. To maintain consistency, they must be primarily responsible for grading. The last thing I should do is to cherry pick and over rule their work.

There are two challenges to project grading. Computer organization is standard material, and the solutions of pass assignments and projects are abundant on the Web. One may say that students who choose to copy solutions waste their time and learning opportunity so who cares, but these are young minds that are often immature, so I do care to at least make it hard for them to fall. Using RISC-V reduces the severity of the problem.

The new problem is ChatGPT and other AI tools which could program in RISC-V. My TAs solved the problem with in-person grading. Students are divided into four groups and come to a TA session each week. They were required to explain their solution. In home work, students wrote and ran RISC-V programs using an emulator. At grading time, TAs set up an actual RISC-V machine so students saw their programs running native and for real.

In one project, the binary bomb, Yifan created the setup that students had practice bombs but when they came to grading, they were given a new bomb to defuse in 15 minutes.

The Result

The end test of a course is how well students have learned after a full semester. There were a total of 869 points across all assignments and exams. The final score is the ratio of student’s points over this total number. Here is the distribution:

50 students scored 80% and above, and all but 7 students were 70% or higher. I had the most fun problem which was deciding between a B+ and an A- for the 8 students who were between 88.94% and 90.2%. This is much better than what I expected from such a difficult course. I remember telling my colleagues who were duly impressed by my students. I am still immensely proud of what they have done.

Parting Thoughts

“One might as well say he has sold when no one has bought as to say he has taught when no one has learned.”
— John Dewey in Logic The Theory of Inquiry

The course has its problems that can and should be improved. One that’s difficult to fix is that students learned RISC-V and then read the CS:APP textbook which uses x86. Right now, they have to map the book examples to RISC-V themselves. The evaluation score is 3.53 for overall instructor and 3.4 for the course, lower than my typical scores (here and here). Seven respondents gave the highest rating, and two the lowest. I appreciate students wrote in the evaluation and in public (here). What’s online is anecdotally true but not complete or comprehensive. My blog is partly to tell the part of the extensive learning that computer science students have accomplished in one of their courses in their four-year journey at Rochester.

Acknowledgements: including but not limited to CS staff Ian Ward and Dave Costello; my TAs Yifan, Boyang, Leo, Jacob, Kestor, Yekai, Zack, and Zachary; and my colleague John Criswell (for suggesting the xargs project).

September 3, 2024

CSC 253 Collaborative Software Design Rate My Professor Chen Ding Fall 2023

University of Rochester Computer Science

CSC 253/453 Collaborative Programming and Software Design

Fall 2023 Student Evaluation

Anonymous inputs were collected by the university before the final exam. 9 out of 25 students (36%) submitted the evaluation.

The overall Instructor Rating is 4.89, same as the overall Course Rating.

All nine students gave highest or next highest score to the questions:

  • Teaching Skills
  • Rapport with Students
  • Academic Honesty
  • Value of the Course

Some of the comments include:

  • I particularly relished the final big project, which was both challenging and immensely rewarding. Working collaboratively with my team was a highlight, fostering a sense of friendship and shared purpose that made the learning process especially enjoyable. However, I do wish we had more time allocated for this final project. The complexity and scale of the project made it engaging, and having additional time would have allowed us to delve deeper into the coding challenges and explore more creative solutions as a team.
  • hard course
  • This course has a strong emphasis on collaboration, which is very helpful for my future work. Project is a little bit hard and it takes a lot of time.

Related posts:

January 10, 2024

CSC 252/452 Computer Organization (Spring 2024)

Chen Ding, Professor of Computer Science
WFs 3:25pm to 4:40 Gavett 206

CSC 252 teaches the fundamentals of modern computer organization, including software and hardware interfaces, assembly languages and C, memory hierarchy and program optimization, data parallelism and GPUs. It shows the underlying physical reality which the virtual world including AI is built and depends on.

Textbooks

Introduction to Programming with RISC-V by Borin, https://riscv-programming.org/book/riscv-book.html, required: §1 to §7.

Computer Systems: A Programmer’s Perspective 3rd Edition by Bryant and O’Hallaron, required: §1, §4.1-4.4, §5 to §12.

CUDA C++ Programming Guide https://docs.nvidia.com/cuda/cuda-c-programming-guide/index.html §1 to §3.2.4 (including §3.2.4), §4, and §5. 

For all other information, see Blackboard.

Except for using RISC-V as the main assembly language (rather than x86), the course is similar to the Spring 2023 course taught by Professor Yuhao Zhu. The previous year page also includes a set of past exams, problem sets, and their solutions.

December 30, 2022

CSC 579 Machine-Checked Proofs Using Coq

CSC 579 Spring 2023
(R 9:40am to 10:55 Lechase 103)

Syllabus

  • The Need for Training Thought: The Values of Thought. Tendencies Needing Constant Regulation.  Regulation Transforms Inference into Proof.
  • Type Systems.  Operational Semantics. Progress. Type Preservation. Type Soundness.
  • Functional Programming in Coq: Data and Functions.  Proof by Simplification, Rewriting and Case Analysis.
  • Proof by Induction. Proofs Within Proofs.  Formal vs. Informal Proof.
  • Lists, Options, Partial Maps.
  • Basic Tactics: apply, apply with, injection, discriminate, unfold, destruct.
  • Logic in Coq. Logical Connectives: Conjunction, Disjunction, Falsehood and Negation, Truth, Logical Equivalence, Logical Equivalence, Existential Quantification.  Programming with Propositions. Applying Theorems to Arguments. Coq vs. Set Theory: Functional Extensionality, Propositions vs. Booleans, Classical vs. Constructive Logic.
  • Inductively Defined Propositions. Induction Principles for Propositions.  Induction Over an Inductively Defined Set and an Inductively Defined Proposition.
  • The Curry-Howard Correspondence. Natural Deduction. Typed Lambda Calculus. Proof Scripts. Quantifiers, Implications, Functions. Logical Connectives as Inductive Types.
schedule-12-22Download