# C & X Reading Group

## Notes for Category Theory
- Category Theory 2010 ver (by Steve Awodey)
- <Has finished Chapter 1.6 on 08/09/22>
- Finish Chapter 1 by 22/09/22 (read at home)
- Start reading Chap 2 on 22/09/22
- Read 2.1.1~2.6 on 20/10/22 (Need to revisit 2.3 Generalized elements later)
- Finished 3.1
- Plant to read 3.2 onwards on

## Reading in Progress:
- Category Theory 2010 ver (by Steve Awodey)
- <Has finished Chapter 1.6 on 8th Sep>
- Plan to finish Chapter 1 by 22nd Sep (read at home)
- Start reading Chap 2 on 22nd Sep
- Beginning Category Theory <up to Chap 10>
- CBPV by Paul Levy

## Side Note

- Page 14 Category Construction Proofs

## Reading List:
- On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control
- https://doi.org/10.1017/S0956796819000121
- MALL proof nets identify proofs modulo
- https://arxiv.org/abs/1609.04693
- Category Theory in Context (by Emily Riehl)
- https://emilyriehl.github.io/files/context.pdf

## Finished List:

1. Distilling Abstract Machine (10/02/2022)
- https://arxiv.org/abs/1406.2370
2. CBPV by Paul Levy <Intro + Chap 1-3> (17/02/2022)
- https://link.springer.com/book/10.1007/978-94-007-0954-6
3. The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space
- https://ps.uni-saarland.de/extras/wcbv-reasonable/
4. A cost-aware logical framework (2022)
- https://dl.acm.org/doi/abs/10.1145/3498670

## Potential Topics:
1. Linear logic
2. Category Theory

## Related References

### Yannick

Mechanized CBV in Coq:
- https://dl.acm.org/doi/10.1145/3371095

Yannick has build a lot by the `undecidability` library (FOL/SOL/CBV...), maybe we could use it for our later prove?

### Beniamino

Strong reduction cost
- Strong Call-by-Value is Reasonable, Implosively

Weak reduction cost
- Reasonable Space for the lambda-Calculus, Logarithmically.

There is a strong relation of evaluation strategy(strong, weak, non-head) with linear logic, the note is at:
- https://drive.google.com/file/d/1ekPjhXfd1xTSCileo0fem5AdU8p0qidG/view

### CBPV & Linear Logic

https://www.irif.fr/~saurin/Enseignement/LMFI/2018-19/presentation-articles/llcbpv.pdf

### A Cost-Aware Logical Framework in CBPV

https://github.com/jonsterling/agda-calf

### Linear Logic & Cost Model

https://tel.archives-ouvertes.fr/tel-00957653v2/document

### Beginning Catogory Theory

https://www.logicmatters.net/resources/pdfs/BeginCatTheory.pdf

### Category Theory 2005 ver (by Steve Awodey)

http://englishonlineclub.com/pdf/Category%20Teory%20[EnglishOnlineClub.com].pdf

### Category Theory in Context (by Emily Riehl)

https://emilyriehl.github.io/files/context.pdf

### A Categorical Manifesto (by Joseph A. Goguen)

https://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=49B0994A2403A1BDD0A0E4E4F3334E3D?doi=10.1.1.13.362&rep=rep1&type=pdf

### Category for the Working Mathematician

http://www.mtm.ufsc.br/~ebatista/2016-2/maclanecat.pdf

### Formal Category Theory : Adjointness for 2-Categories

https://link.springer.com/content/pdf/10.1007/BFb0061280.pdf

### Sheaves in Geometry and Logic (by Saunders Mac Laneleke Moerdijk )

http://atondwal.org/Sheaves_in_Geometry_and_Logic__MacLane_Moerdijk.pdf