Computability Theory of and with Scheme, Spring 2003

View Resource

Remix and Share

Author:

Meyer, Albert R.

Subject:

Science and Technology

Institution Name:

M.I.T.

Collection:

MIT OpenCourseWare

Grade Level:

Post-secondary

Abstract:

Theory for programmers. Introduction to programming and computability theory based on a term-rewriting, "substitution" model of computation by Scheme programs with side-effects. Computation as algebraic manipulation: provable and valid inequalities for multivariate polynomials. Scheme evaluation as algebraic manipulation and term rewriting theory. Paradoxes from self-application and introduction to formal programming semantics. Undecidability of the Halting Problem for Scheme. Properties of recursively enumerable sets, leading to Incompleteness Theorems for Scheme equivalences. Introduction to logic for program specification and verification. Hilbert's Tenth Problem. Alternate years. 6.844 is a graduate introduction to programming theory, logic of programming, and computability, with the programming language Scheme used to crystallize computability constructions and as an object of study itself. Topics covered include: programming and computability theory based on a term-rewriting, "substitution" model of computation by Scheme programs with side-effects; computation as algebraic manipulation: Scheme evaluation as algebraic manipulation and term rewriting theory; paradoxes from self-application and introduction to formal programming semantics; undecidability of the Halting Problem for Scheme; properties of recursively enumerable sets, leading to Incompleteness Theorems for Scheme equivalences; logic for program specification and verification; and Hilbert's Tenth Problem.

Languages:

English

Material Type:

Full Course, Homework and Assignments, Syllabi, Other

Media Format:

Text/HTML, Downloadable docs

Conditions of Use:

Creative Commons Attribution-Noncommercial-Share Alike 3.0