CS522 Programming Language Semantics

For those students interested in extra review of the various concepts, please see the group/website information posted below.

If you have additional information you feel would benefit the class, please email the webmaster (netid: skeirik2).

 

Spring 2016 Category Theory Reading Group

Every Monday and Wednesday from 3:30-5:00PM

Siebel Center Room 1132

 

For forthcoming lectures, various readings will be posted below which may be necessary

to understand the lecture or may enhance your understanding of the course material.

 

Abbreviations:

STACS - Set Theory and Algebra in Computer Science

STCS - Set Theory in Computer Science

 

Wed. 10:

Required Reading: STACS Sec. 7.4-7.5

Further Reading: STCS Chap. 10

 

Fri. 12:

Required Reading: scanned pages in Ohlebusch's book Advanced Topics in Term Rewriting
Further Reading: Hirokawa et al. Leftmost Outermost Revisited Sec. 1-3

Wed. 17:
Required Reading: pgs. 1-19 of Meseguer and Marti-Oliet General Logics and Logical Frameworks
Further Reading: Aczel Schematic Consequence, Gougen and Burstall Institutions

Fri. 19:
Required Reading: Meseguer General Logics Sec. 3.1, 3.2, and 6
Further Reading: Meseguer From OBJ to Maude and Beyond, Meseguer and Duran Proving Operational Termination of Declarative Programs in General Logics, and Structured Theories and Institutions

Wed. 24:
Required Reading: Meseguer Twenty Years of Rewriting Logic up to Sec. 3.3 (focus on Sec. 3.3), Van Emden and Kowalski The Semantics of Predicate Logic as a Programming Language
Further Reading:

• Escobar Functional Logic Programming In Maude
• Meseguer and Gougen Models and Equality for Logic Programming
• Meseguer and Thati Symbolic Reachability Analysis via Narrowing and its Application to Verification of Cryptographic Protocols
• Jaffar and Maher Constraint Logic Programming: A Survery
• Escobar et. al Folding Variant Narrowing and Optimal Variant Termination

Fri. 26:
Required Reading: Selinger Lecture Notes on the Lambda Calculus (available above) Sec. 2 & 3
Further Reading: Church An Unsolvable Problem of Elementary Number Theory

Wed. 2:
Required Reading: Term Rewriting Systems Sec. 3.3, CL.maude, Lecture 13 Addendum
Further Reading: Shoenfinkel On The Building Blocks of Mathematical Logic, Turner A New Implementation Technique for Applicative Langauges

Fri. 4:
Required Reading: Selinger Lecture Notes on the Lambda Calculus (available above) Sec. 4, Lecture 14 Addendum, lambda.maude

Wed. 9:
Required Reading: Stehr CINNI - a Generic Calculus of Explicit Substitutions Sec. 1-4, 5.1, and 5.3, De Bruijn Notation Notes from Cornell, lambda-DB+CINNI.maude
Further Reading:

• Aczel A General Church Rosser Theorem
• Berkling and Fehr Extensions of Lambda Calculus as Basis for Programming Languages
• De Bruijn "Namefree" Lambda Calculus
• Curien et. al Confluence Properties of Weak and Strong Calculi of Substitutions

Fri. 11:
Required Reading: Meseguer General Logics Sec. 5 (link above), Meseguer and Marti-Oliet Inclusions and Subtypes I pgs. 409-424 (excl. Sec. 3.2)

Wed. 16:
Required Reading: CS522 Lectures 16 and 17 Notes Part I & Part II (notes: pgs. 1-12 excl. Sec. 2.1 were already covered in the lecture on Fri. 11th; part II contains corrections for part I)

Fri. 18 Lectures 1 & 2:
Required Reading: Selinger Lecture Notes on the Lambda Calculus (available above) Sec. 6, Meseguer and Marti-Oliet Inclusions and Subtypes II
Further Reading:

• Tannen Combining Algebra and Higher Order Types
• Girard et. al Proofs and Types Chap. 3-4 (available above)
• Curien Categorical Combinators
• Hardin Confluence Results for the Pure Strong Categorical Logic CCL

Wed. 30:
Required Reading: Meseguer STACS Chap. 8-9 and Martin Löf An Intuitionistic Theory of Types: Predicative Part, Lecture Notes on Curry-Howard Isomorphism
Further Reading: Martin Löf Constructive Mathematics And Programming, Intuitionistic Type Theory, Nordström et. al Programming In Martin Löf's Type Theory (available above)

Wed. Apr. 13:
Required Reading: Seely Locally Closed Cartesian Categories and Type Theory, Mesguer Notes for the Seely Paper
Further Reading: Jacobs Comprehension Categories and the Semantics of Type Dependency

Fri. Apr. 15:
Required Reading:

• Reynolds Type Abstraction and Parametic Polymorphism
• Selinger Lecture Notes on the Lambda Calculus (avaialable above) Sec. 8
• Meseguer Relating Models of Polymorphism
• Meseguer Polymorphic Lambda Calculus Notes

Further Reading:

• Seely Categorical Semantics for Higher Order Lambda Calculus
• Proofs and Types (available above) Chap. 11
• Huet and Coquand Calculus of Constructions
• Stehr and Meseguer Pure Type Systems in Rewriting Logic
• Reynolds Theories of Programming Languages (Chap. 17)
• Simpson et. al Comprehensive Parametric Polymorphism: Categorical Models and Type Theory
• Reynolds Towards a Theory of Type Structure
• Gougen Higher Order Functions Considered Unnecessary for Higher Order Programming
• Strachey Fundamental Concepts of Programming Languages (focus on Sec. 3.6)

Wed. Apr 20:
Required Reading: Meseguer and Rosu The Rewriting Logic Semantics Project: A Progress Report, Reynolds Theories of Programming Languages (Chap 2.), Meseuger Denotational vs. Algebraic Semantics Notes
Further Reading:

• Scott and Strachey Towards a Mathematical Semantics for Computer Languages
• Mosses and Gunter Semantic Domains and Denotational Semantics
• Reynolds Theories of Programming Languages (Chap. 5)
• Wand First Order Identities as a Defining Language
• Gougen and Parsaye-Ghomi Algebriac Denotational Semantics Using Parameterized Abstract Modules

Fri. Apr 22:
Required Reading: Serbanuta et. al A Rewriting Logic Approach To Operational Semantics
Further Reading:

• Kahn Natural Semantics
• Plotkin A Structural Approach To Operational Semantics
• Mosses Modular Structural Operational Semantics
• Wright and Felleisen A Syntactic Approach to Type Soundness
• Berry and Boudol The Chemical Abstract Machine