Elektrine lite

← Feed

Carlo Angiuli

carloangiuli@mathstodon.xyz

<p>Assistant Professor in Computer Science at Indiana University. Into (homotopy) type theory &amp; programming languages.</p>

Posts

  • View post

    @danielgratzer@mathstodon.xyz and I have just released a new version of _Principles of Dependent Type Theory_! This one is a significant milestone: all planned content has been drafted; we do not expect any new sections at this point. Main changes: - Added Appendix B on generalized algebraic theories! This resolves some unfinished business from earlier in the book, by proving the &quot;initiality theorem&quot; for ETT/ITT. - Added a draft of Section 4.4 on observational type theory. - Removed &...

  • View post

    RE: https://mathstodon.xyz/@danielgratzer/117003175661766753 We are working together in Daniel’s office, and every time his computer dings with another like on this post, he looks at me like 😏

  • View post

    In a previous wave of Lean discourse, there was discussion about the fact that type-checking a Lean file can run arbitrary code. There are pros and cons to this, but one particularly obvious con is, well, let&amp;#39;s just hear Kevin Buzzard&amp;#39;s version: &amp;quot;One cannot trust AI-generated code so I ran [the AI-generated formalization of the Erdős unit distance conjecture counterexample] in a sandbox on my machine (malicious Lean code can run arbitrary commands on your computer — Lea...

  • View post

    Went to lunch today with the PL grad students, who started discussing their relatively large range of ages. Student 1: Well, I&amp;#39;m 24. Me: I mean, isn&amp;#39;t that the age Coolio said he wasn&amp;#39;t sure if he&amp;#39;d live to see? Student 2: Who&amp;#39;s Coolio? Student 3: That&amp;#39;s a musical artist, right? Student 2: ...from the 1900s? [@samth and I are dying]

  • View post

    PCF is a domain-specific language for ω-cppos.

  • View post

    17th century mathematical mistakes: I have a proof that is too large to fit in this margin. 21st century mathematical mistakes: I have a file that is too large to fit in this buffer.

  • View post

    Does anybody here have any opinions about the candidates in the ACM general election, vis-à-vis the Digital Library, ACM financials, or other hot-button issues?

  • View post

    LICS paper with @trebor accepted! 🎉

  • View post

    As you might have guessed, meeting the requirements is not quite the same as actually making one&#39;s mathematics very accessible. I&#39;m interested in figuring out how to actually do the latter by instrumenting my macros to generate helpful alt text, but that project will have to wait a few months.

  • View post

    I had totally forgotten about this slide deck about gluing from years ago...