Skip to content
View SyntakticSugar's full-sized avatar

Block or report SyntakticSugar

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this userโ€™s behavior. Learn more about reporting abuse.

Report abuse
SyntakticSugar/README.md

Hello, my name is Robert ๐Ÿ‘จโ€๐Ÿ’ป

My interests are in functional programming, logic, type theory, and category theory. I enjoy writing code in Racket, Haskell, Agda, and Lean.

Projects ๐Ÿ—๏ธ

I spend most of time split between refining my course materials and adding to my digital library of mathematics. However, I make other projects available on here too.

Vocation

I am a mathematics teacher in Christchurch, New Zealand. I am primarily involved with teaching first year undergraduates, but I do teach a second year class about logic and computation. I studied mathematics at the University of Canterbury (BSc Hons) and Australian National Univeristy (PhD) primarily studying algebraic geometry, algebraic number theory, and category theory. I wrote my thesis about Grothendieck's Galois Theory of schemes over the natural numbers. My interests have moved towards type theory, in particular as a language to express mathematics.

Pinned Loading

  1. lamb lamb Public

    Reduction of untyped lambda terms ๐Ÿ‘ written in Haskell.

    Haskell

  2. magicy magicy Public

    Y Combinator magic ๐Ÿง™โ€โ™‚๏ธ computed ๐Ÿช„ by Racket

    Racket

  3. turing turing Public

    Turing Machine interpreter ๐Ÿ written in Python.

    Python

  4. mathematics mathematics Public

    Libary of mathematics ๐Ÿ“š formally verified in Lean 4 โœ…

    Lean

  5. proofgrams proofgrams Public

    Course notes ๐Ÿ“” logic, lambda calculi, and Curry-Howard

    TeX