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.
C311/B521 Programming Languages | Spring22 → Spring23
B555 Machine Learning | Fall23
C343 Data Structures | Spring24