Contact: cd17@iu.edu | Github: dcclogin | Office: TBA

I am a Ph.D. student in the Department of Computer Science at Luddy School of Informatics, Computing, and Engineering (SICE), Indiana University Bloomington. I once majored in Bioinformatics at Shanghai Jiao Tong University. My interests range from theoretical aspects of programming languages to philosophy. I am currently exploring Homotopy Type Theory and its computational models; personally interested in inscription of radical physicality - a variety of intensional properties into the very extensional notion of mathematical and classically computaional functions…(time, space, velocity, information effects, quantum effects, and so on)

I extended A circuit-like notation for lambda calculus to an informal “topological” model of λ-calculus - λ-circuits. Partial evaluation and supercompilation can be shown clearly with them. You can also view them as an alternative approach to natural deduction and Gentzen style reasoning, but they are not eligible to cover dependent types and beyond intuitively. I did this mainly for fun, and out of some minimalistic beliefs.

I have been reading German philosophers (from Kant to Husserl), Buddhism and classical Chinese thoughts. I have a strong urge to reconcile programming-language/math/logic and continental philosophy. My favorite reading stuff are from Jean-Yves Girard, Alain Badiou, and Slavoj Žižek.

My philosophical, mathematical, logical, computaional, physical, and political obsessions locate themselves in the very concept (or the huge constellation of concepts) of ‘negation’/‘negativity’ (Hegel) and ‘equalities’/‘equivalences’ (Ontology). To much to be articulated in my future posts…

Cubical Sqrt - (In progress) an experimental project on reversible programming, quantum computing, and cubical type theory.

λ-Circuit - a graphical prototype language of lambda calculus.

- 主义主义 - about ideology and philosophy (Chinese only).
- The Little Learner - a straight line to deep learning.
- EuclideanSpace - Mathematics and Computing - full of diagrams.
- John Baez’s Blog - stuff on physics and category theory.
- Graphical Linear Algebra - a fresh view, and a diagrammatic approach.
- 1lab - detailed explanation and full implementation of cubical type theory.
- The n-Category Café - on math, physics and philosophy.
- EPIT Spring School on HoTT - a gentle introduction to dependent types and HoTT.

C311/B521 Programming Languages | Spring22 → Spring23

B555 Machine Learning | Fall23