This course concentrates on general-purpose models of computation, incorporating non-classical aspects like concurrency and interaction.

Prerequisite: Models of
Computation

There will be an exam on January 28.

- Basic models: (multidimensional) Turing machines; recursive functions [Thue systems (type 0 grammars)]
- Rewriting models of nondeterminacy, including lambda calculus,
combinatory logic, and typed systems

- Abstract state machines, including effectiveness, parallelism, and interaction
- Cellular automata, Petri nets, and membrane systems, as models of concurrency
- Analog computation

- [Quantum computing and other invertible models]

- Introduction
- The Recursive Function Model
- Primitive recursion and recursion (Chap. 4 in Ref. #1 or any other source)
- Comparing models (Ref. #8)
- Representations

- The Lambda Calculus Model
- Rewriting Models
- Church-Rosser Theorems (Ref. #3)
**HW #1**(due end Nov.)

- Abstract State Machines (Ref. #4)
- Parallel Models (Guest lecture: Jenny Falkovich)
- Oracular Models
**HW #2**(due end Dec.)

- Effective Models (Ref. #9)
- Typed Models (Ref. #10, Ref. #11)
- Normalization
- Petri Nets (Ref. #6)
- Cellular Models (Ref. #13; Ref . #12)
- Analog Models

*Models of Computation: An Introduction to Computability Theory*, Maribel Fernández, Springer, 2009*Programming Languages and Lambda Calculi,*Matthias Felleisen and Matthew Flatt, 2006- "Rewrite
Systems", Nachum Dershowitz and Jean-Pierre Jouannaud,
*Handbook of Theoretical Computer Science, vol. B: Formal Methods and Semantics*, chap. 6, North-Holland, 1990 *The Expressive Power of Abstract-State Machines*, Wolfgang Reisig,*Computing and Informatic*s, 2003

*Cellular Automata: Models for a Discrete World*, Joel Schiff, Wiley, 2007 (Chap. 3 online)*Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies*, Wolfgang Reisig, Springer, 2013- "Sequential Abstract State Machines
Capture Sequential Algorithms", Yuri Gurevich,
*ACM TOCL,*2000 - "Comparing
Computational Power", Nachum Dershowitz & Udi Boker,
*Logic J. of IGPL,*2006 - "A
Natural Axiomatization of Computability and Proof of Church's
Thesis, Nachum
Dershowitz & Yuri Gurevich,
*Bull. Symbolic Logic,*2008

- "Lambda
Calculus with Types", Henk Barendregt, in P
*erspectives in Logic,*Cambridge University Press, 2013

*Proofs and Types*, Jean-Yves Girard- "Causal
Graph Dynamics", Pablo Arrighi and Gilles Dowek,
*Inf. Comput.,*2013 *Cellular Automata*, Jarkko Kari*A New Kind of Science*, Stephen Wolfram