About myself
I'm Dr. Gergő Érdi (Érdi Gergő in the original Hungarian order of surname first), born on 18th November, 1980 in Budapest. In 2011 I've moved to Singapore.
I graduated from Semmelweis University of Medicine with an MD in 2005. Meanwhile, in 2003 I also started studying at the Computer Science faculty of Eötvös Loránd University, and got my CS master's degree in 2011.
Between 2005 and 2011, I've worked at Intentional Software. Since 2011, I'm currently at Standard Chartered Bank.
Simply Typed Lambda Calculus in Agda, Without Shortcuts
1 May 2013 (programming agda correctness language)There are many ways to introduce dependent type systems, depending on which side of the Curry-Howard lens you look through. But if your interest is more in programming languages than proof assistants, then length-indexed vectors is your Hello, World!, and an interpreter for the simply-typed lambda calculus is your FizzBuzz. I think the usual presentation of the latter is a bit of a cheat, for reasons which I will explain below. I'll also show a "non-cheating" version.
Continue reading »Older entries
My software
I hack on the following free software projects in my free time. Way back, most of them were either part of the GNOME project, or were based on the GNOME platform. These days, I'm mostly just writing small programs for fun, or throw-away code relevant to some theoretical subjects I happen to get interested in in the field of functional programming.
- Guikachu: Graphical resource editor for the GNU PalmOS SDK
- Alef: A lazy functional programming language (interpreter and compiler)
- MetaFun: Compile a Haskell-like functional language into C++ template metaprograms
- Tandoori: Compositional type checker for Haskell 98 (my M.Sc. thesis)
Smaller ones
- Collection of Elisp snippets.
- Goblin: A Python implementation of the board game Gobblet, for Windows and Unix/Linux systems.
- XSLT templates for creating your CV: This page describes in detail a simple way to generate HTML and printable versions of your resume from a single source.