Logic in Computer Science, Engineering and Industry
summary
Survey links classical logic results to concrete engineering: types powering modern languages and Java/.NET virtual machines; deterministic pushdown parsing (LR) actually revolutionizing compilers; model-theoretic ideas explaining order-independence in SQL; many-valued logics arising from analog circuit tolerances; abstract state machines giving a formal model for algorithms across levels of abstraction; practical tools like Spec Explorer and the Terminator halting analyzer that succeed on real C code and SMT-style solvers that underpin verification.
AI-written summary · about
chapters (21)
- 0:00Intro
- 0:40Types
- 2:58Computability
- 3:51Recursion in CS
- 4:16Lambda calculus
- 4:26Machines
- 7:49Model theory
- 9:13Proof theory → logic engines
- 9:34Finite automata
- 10:42Levels of abstraction
- 11:25One under-appreciated achievement
- 13:18Software engineering V-diagram
- 14:24Software specifications
- 16:45Electrical engineers have been using logic explicitly
- 19:26Proliferation of formal languages
- 20:27Logic day in and day out
- 23:00Engineers do not know logic
- 24:46Syntax divide: precise vs. "precisable"
- 25:06Semantics divide
- 25:50Feasibility divide
- 27:01Declarative/operational divide
related talks
52mThink Abstractly, Work Concretely
15mCurrent Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can Do Better
11mIntroduction
32mDesign of Software Representation Languages: a Historical Perspective
23mFormal Methods to Save the Earth
01h 05mFour Languages from Forty Years Ago
34mAbstract Interpretation, Software Model Checking, and Beyond - A Celebration of the(…)
01h 05mVerifying Infinitely Many Programs at Once