Formal Semantics of Programming Languages: From Lambda Calculus to Separation Logic
Review
期末考试
•
时间
：
2021
年
12
月
23
日周四
1-2
节
，
8:00-9:50
•
地点
：
上课教室
（
逸
B-205
）
•
闭卷
•
总成绩
：
作业
40% +
考试
60%
•
答疑
：
不统一安排
，
可发邮件或
群讨论
Formal Semantics of Programming
Languages
•
Lambda Calculus
•
Untyped
•
Simply typed
•
Imperative languages
•
Operational semantics
•
Hoare logic
•
Separation logic
Untyped lambda calculus
•
Syntax
•
Semantics (reduction rules)
Simply-typed lambda calculus
•
Syntax
•
Reduction rules
Simply-typed lambda calculus
•
Typing rules
A simple imperative language
•
Syntax
Operational semantics
•
Small-step
Operational semantics
•
Big-step
Hoare logic
•
Hoare triple validity
•
Inference rules for partial correctness
Separation logic
•
The extended programming language
•
Syntax & operational semantics
Separation logic
•
The assertion language
Separation logic
•
Locality
•
Safety monotonicity
•
Frame property
Formal Semantics of Prog. Lang.
•
Lambda Calculus
•
Untyped
•
Reduction
•
Simply typed
•
Reduction vs typing : progress & preservation
•
Imperative languages
•
Operational semantics
•
Small-step & big-step
•
Hoare logic
•
Reasoning using Hoare logic
•
Separation logic
•
Assertion semantics & locality
Explore the foundational concepts of formal semantics in programming languages, covering Lambda Calculus, Untyped and Simply-typed languages, Imperative languages, Operational and Hoare logics, as well as Separation logic. Delve into syntax, reduction rules, typing rules, and operational semantics in various language paradigms.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Formal Semantics of Programming Languages Lambda Calculus Untyped Simply typed Imperative languages Operational semantics Hoare logic Separation logic
Untyped lambda calculus Syntax Semantics (reduction rules)
Simply-typed lambda calculus Syntax Reduction rules
Simply-typed lambda calculus Typing rules
A simple imperative language Syntax
Operational semantics Small-step
Operational semantics Big-step
Hoare logic Hoare triple validity Inference rules for partial correctness
Separation logic The extended programming language Syntax & operational semantics
Separation logic The assertion language
Separation logic Locality Safety monotonicity Frame property
Formal Semantics of Prog. Lang. Lambda Calculus Untyped Reduction Simply typed Reduction vs typing : progress & preservation Imperative languages Operational semantics Small-step & big-step Hoare logic Reasoning using Hoare logic Separation logic Assertion semantics & locality
