Course work: CPSC 701.04: Proof theory and Linear Logic

Lecture notes for Proof Theory

Lecture notes from first class, 2006-09-13, introduction to Sigma-Pi logic, discussion of Curry-Howard-Lambek isomorphism. Examples of proofs in Sigma-Pi.
page0001 page0002 page0003 page0004 page0005  
page0006 page0007 page0008 page0009 page0010  
Lecture notes from second class 2006-09-15. Cut theorem and rewritings for Sigma-Pi, annotations of proofs.
page0011 page0012 page0013 page0014 page0015  
page0016 page0017 page0018 page0019 page0020  
Lecture notes from third class 2006-09-20. Discussion, motivation and proof of confluence for rewritings for Sigma-Pi.
page0021 page0022 page0023 page0024 page0025  
page0026 page0027 page0028 page0029 page0030 page0031
Lecture notes from fourth class 2006-09-22. Proof that Sigma-PI(A) is a category when A is a Category.
page0032 page0033 page0034 page0035 page0036  
page0037 page0038 page0039 page0040    
Lecture notes from fifth class 2006-09-27. Discussion of poly categories and views as a process.
page0041 page0042 page0043 page0044 page0045 page0046
page0047 page0048 page0049 page0050 page0051  
Lecture notes from sixth class 2006-09-29. Continue discussion of poly categories, views as a process and relationship to multiplicative linear logic.
page0052 page0053 page0054 page0055 page0056 page0057
page0058 page0059 page0060 page0061 page0062  
Lecture notes from seventh class 2006-10-04. Work through "boxing" of a graph and the proof of Girard's switching theorem.
page0063 page0064 page0065 page0066 page0067  
page0068 page0069 page0070 page0071 page0072  
Lecture notes from eighth class 2006-10-06. Discuss "Empires" and switch conditions.
page0073 page0074 page0075 page0076    
page0077 page0078 page0079 page0080    
Lecture notes from ninth class 2006-10-11. Discuss categorical semantics of cut - multiplicative linear logic. Introduction of Linear Distributive Categories. Chu construction.
page0081 page0082 page0083 page0084 page0085  
page0086 page0087 page0088 page0089 page0090  
Lecture notes from tenth class 2006-10-13. Discuss negation in LL, *-autonomous categories, dualizing objects.
page0091 page0092 page0093 page0094 page0095  
page0096 page0097 page0098 page0099    
Lecture notes from eleventh class 2006-10-25. Discuss additives of LL, extension of the additive term logic (Cockett, Pastro)
page0100 page0101 page0102 page0103 page0104 page0105
Lecture notes from twelveth class 2006-10-27 (Sean Nichols). Discuss message passing logic.
page0106 page0107 page0108 page0109    
page0110 page0111 page0112      
Lecture notes from thirteenth class 2006-11-01. Discuss initial algebras, final co-algebras and how datatypes arise from this.
page0113 page0114 page0115 page0116 page0117  
page0118 page0119 page0120 page0121 page0122  
Final lecture of part 1, fourteenth class 2006-11-03. Continue discussion of datatypes, Bekic lemma, circular definitions.
page0123 page0124 page0125 page0126    
page0127 page0128 page0129 page0130    
Last modified by Brett Giles
Last modified: 2012-11-19

Valid HTML5