-
Notifications
You must be signed in to change notification settings - Fork 3
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
aefd94f
commit a1ba16a
Showing
56 changed files
with
99 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,39 @@ | ||
+++ | ||
draft = false | ||
title = 'AAA528-18F' | ||
+++ | ||
|
||
# Computational Logic, 2018 Fall | ||
|
||
## Course Information | ||
|
||
- Instructor: [Hakjoo Oh]({{< ref "/members/hakjoo-oh.md" >}}) | ||
- Lecture: 9:00-11:30 on Mondays | ||
|
||
## Slides | ||
|
||
- Course Overview: [lec0.pdf](./slides/lec0.pdf) | ||
- Propositional Logic: [lec1.pdf](./slides/lec1.pdf), [lec2.pdf](./slides/lec2.pdf) | ||
- First-Order Logic: [lec3.pdf](./slides/lec3.pdf), [lec4.pdf](./slides/lec4.pdf), [lec5.pdf](./slides/lec5.pdf) | ||
- Program Verification: [lec6.pdf](./slides/lec6.pdf), [lec7.pdf](./slides/lec7.pdf), [Hoare Logic](./slides/HoareLogic-6up.pdf) | ||
- Decision Procedures: [lec8.pdf](./slides/lec8.pdf), [Equality Theory](./slides/lecture11-6up.pdf), [Theory of Rationals](./slides/lecture12-6up.pdf), [Nelson-Oppen](./slides/lecture16-6up.pdf) | ||
|
||
## Homework | ||
|
||
- Homework 1: [hw1.pdf](./homeworks/hw1.pdf) (due 10/01) | ||
- Homework 2 (Reading): [SMT: Introduction and Applications](./homeworks/p69-de_moura.pdf) (due 10/29, submit 2-pages summary) | ||
- Homework 3: Exercises 1 and 2 in Lecture 7 (due 11/12) | ||
|
||
## Resources | ||
|
||
- SAT/SMT Solvers: | ||
- [Tutorial on Z3](https://rise4fun.com/z3/tutorial) | ||
- Applications of SAT/SMT Solvers: | ||
- [Symbolic Execution](./misc/SymbolicExecution.pdf) | ||
- [Dynamic Symbolic Execution](./misc/DynamicSymbolicExecution.pdf) | ||
- [Bounded Model Checking](./misc/BoundedModelChecking.pdf) | ||
- [Smart Contract Verification](./misc/ContractVerification.pdf) | ||
- [Automatic Debugging](./misc/fse18.pdf) | ||
- [Intelligent Tutoring System](./misc/oopsla18-fixml.pdf) | ||
- Related topics: | ||
- [Abstract Interpretation](./misc/AbsInt.pdf) |
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,55 @@ | ||
+++ | ||
draft = false | ||
title = 'COSE212-18F' | ||
+++ | ||
|
||
# Programming Languages, 2018 Fall | ||
|
||
## Course Information | ||
|
||
- Instructor: [Hakjoo Oh]({{< ref "/members/hakjoo-oh.md" >}}) | ||
- Lecture: 15:30-16:45 on Mondays and Wednesdays | ||
- [Syllabus](./syllabus.pdf) | ||
|
||
## References | ||
|
||
- [Essentials of Programming Languages](http://www.amazon.com/gp/product/0262062798?ie=UTF8&tag=ucmbread-20&linkCode=as2&camp=1789&creative=9325&creativeASIN=0262062798) | ||
{{< figure src="./eopl.jpg" width="100px" link="http://www.amazon.com/gp/product/0262062798?ie=UTF8&tag=ucmbread-20&linkCode=as2&camp=1789&creative=9325&creativeASIN=0262062798" target="_blank" >}} | ||
- [Notes on Programming Languages (in Korean)](./pl-book-draft.pdf) | ||
|
||
## Slides | ||
|
||
- Course Overview: [lec0.pdf](./slides/lec0.pdf) | ||
- (Part 1) Preliminaries | ||
- Inductive Definitions: [lec1.pdf](./slides/lec1.pdf), [lec2.pdf](./slides/lec2.pdf) | ||
- Functional Programming: [lec3.pdf](./slides/lec3.pdf), [lec4.pdf](./slides/lec4.pdf) | ||
- (Part 2) Basic Concepts | ||
- Expressions: [lec5.pdf](./slides/lec5.pdf) | ||
- Procedures: [lec6.pdf](./slides/lec6.pdf) | ||
- Lexical scoping: [lec7.pdf](./slides/lec7.pdf) | ||
- States: [lec8.pdf](./slides/lec8.pdf) | ||
- Records, Pointers, and GC: [lec9.pdf](./slides/lec9.pdf) | ||
- (Part 3) Advanced Concepts | ||
- Static Type System: [lec10.pdf](./slides/lec10.pdf), [lec11.pdf](./slides/lec11.pdf), [lec12.pdf](./slides/lec12.pdf) | ||
- Automatic Type Inference: [lec13.pdf](./slides/lec13.pdf), [lec14.pdf](./slides/lec14.pdf), [lec15.pdf](./slides/lec15.pdf) | ||
- Polymorphic Type System: [lec16.pdf](./slides/lec16.pdf) | ||
- Lambda Calculus: [lec17.pdf](./slides/lec17.pdf) | ||
- Review: [lec18.pdf](./slides/lec18.pdf), [intro to PL research](./slides/research_intro.pdf) | ||
|
||
## Homework | ||
|
||
**[System for programming assignments](https://tryml.korea.ac.kr)** | ||
|
||
- Homework 1 (Functional Programming 1) [hw1.pdf](./homeworks/hw1.pdf) (due 09/30 24:00) | ||
- Homework 2 (Functional Programming 2) [hw2.pdf](./homeworks/hw2.pdf) (due 10/14 24:00) | ||
- Homework 3 (Interpreter for Functional Language) [hw3.pdf](./homeworks/hw3.pdf) (due 10/28 24:00) | ||
- Homework 4 (Interpreter for Imperative Language) [hw4.pdf](./homeworks/hw4.pdf) (due 11/11 24:00) | ||
- Homework 5 (Static Type System) [hw5.pdf](./homeworks/hw5.pdf) (due 12/16 24:00) | ||
|
||
## Previous Exams | ||
|
||
- [Final Exam (2017)](./exams/final2017.pdf) | ||
- [Final Exam (2016)](./exams/final2016.pdf) | ||
- [Final Exam (2015)](./exams/final2015.pdf) | ||
|
||
## Reading |
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.