hello, world!

I'm Ioanna, a software engineer in Bonn. Welcome to my homepage.

Browse:

• about me
• software projects
• peer reviewed publications
• my posts

about me

Short version:

I'm a software engineer, a doctor in mathematical logic, and I'm greek chilean, thus the two first names and two last names. I've taught a lot, and I've worked on set theory, medical statistics, formal proving (maths), graphing software, frontends and backends, search engines, container software, and networking software, among other smaller projects. Currently I'm an Igalian, working with the compilers team of Igalia. Now it's hard for me to think about anything other than compilers, a truly applied logic part of programming.

In some more detail:

• Grew up in Thessaloniki, where I studied mathematics.
• Did my master's degree in logic in Amsterdam.
• Finished my Dr.rer.nat. degree in set theory in 2011 in Bonn, where I live now.
• Afterwards I worked in medical statistics at the university clinic of Bonn, where I decided I like programming more.
• Then I joined a project in formal mathematics and automated reasoning in ML and OCaml. You can see me talk about this on youtube during FOMUS.
• For many years until 2017, I taught and tutored mathematics to bachelors and masters students and to school kids.
• I'm a software engineer, and a Common Lisper since 2014, thanks to Interstellar.
• I wrote the Choiceless Grapher almost from scratch, for my former colleagues in set theory.
• During 2017-2019 I worked on search engines (ELK), containers, docker, kubernetes, AWS, and openshift, as well as some Python AI projects.
• Since January 2019 I can't stop reading about compilers. Papers on transformations (passes) between intermediate representations, i.e., formal languages, may be thought of in terms of natural deduction, a comfortable place for a logician.
• On November 2019, I joined Igalia full time as part of their compilers team, and I am over the moon! Currently I'm happily on the WebAssembly team.
• I love all Lisps and every year I go to the European Lisp Symposium (ELS). I am chairing the 2020 edition, and for this reason, the special focus of ELS2020 is "compilers".

My favourite languages, vaguely ordered: Common Lisp, Scheme, WebAssembly, R, OCaml, APL (yes, APL), Python, Haskell, Shell (love and hate), and as a logician of course lambda calculus (untyped as a set theorist and typed as a formalist).

I speak four human languages: Greek, English, German, Spanish, and I can still understand some Dutch.

software projects

An incomplete list of my software projects. For my logic and for my statistics projects see publications.

lambda

A toy compiler of the untyped lambda calculus into common lisp (so far), written in common lisp, with an interpreter and a user interface (UI). The UI includes two REPLs and a viewer of all available transformations, or representations, of a user-input λ term. Showcases representations of lambda terms in my quest to understand compilers.

• Features a User Interface (UI) which includes:
  • A basic REPL "λ.base", which allows you to input λ terms which use the following symbols as primitives: :ID :TRUE :FALSE :S :AND :OR :IF :Y :OMEGA
  • A church numeral calculator REPL "λ.church", which allows you to use λ.base, as well as numbers in your statements, and the following symbols as primitives for numeric functions: :A+ :A* :Aexp :Azero? :A+1 :A-1 :A-factorial, for plus, times, exponent, zero test, successor, predecessor, and factorial.
  • A transformation viewer: Input a λ term and see its available representations, so far features the standard syntax with and without primitives, the de Bruijn representation, and the common-lisp syntax.
• Compiles to Common Lisp functions. Compiler transformations and simplifications are currently only β-reducing in normal order with loop-catching and maximum allowed steps, closing possibly open terms, full renaming of bound variables, then switching to common-lisp syntax and returning the resulting common-lisp closure.
• For more features and more details see the README and the comments in the code.
• Code https://gitlab.common-lisp.net/idimitriou/lambda

cgraph.inters.co

A diagram maker for relationships between certain axioms of set theory.

• Try it: https://cgraph.inters.co.
• See the source code: https://gitlab.common-lisp.net/idimitriou/jeffrey
• There are descriptions in the links above, and three detailed articles on Cgraph will appear as notes.

asd-graph

Dependency grapher for Common Lisp projects.

• Graphs the dependencies between files and modules defined in an .asd file.
• TBA: Graphing the dependencies and exported functions in packages defined in a packages.lisp file.
• Description, source code and installation instructions: https://gitlab.common-lisp.net/idimitriou/asd-graph
• In the shiny-R branch, you can deploy a Shiny server, using R, which serves a website with a file-form input, which when given an .asd file with a system definition, dynamically graphs that system. In Shiny R because it creates dynamic websites and because I love R, too.

nbg-hol

Group project:
With the mathematical logic group of Bonn, that is Prof. Koepke and 11 bachelors and masters students doing a formal mathematics internship, we did a formalisation of von Neumann-Bernays-Gödel Set Theory of classes in Isabelle.

• Discovered that proof assistants are very powerful in their theorem proving tactics suggestions (Sledgehammer), and that it's easy to define a language in a type theoretic way, create constructors, and prove theorems about that language, building up an axiomatic system.
• We used the Isar proving language, which makes formal proving very accecible to beginners.
• You can see me present this project on youtube during FOMUS, where I spent a lovely week talking with category and type theorists, who are pleasantly quite direct about their opinions.

my repositories

For more software projects take a look here:

• Common-lisp projects: https://gitlab.common-lisp.net/idimitriou
• All projects: https://github.com/ioannad

peer-reviewed publications

All uncountable cardinals in the Gitik model are almost Ramsey and carry Rowbottom filters, Arthur Apter, Ioanna Dimitriou, and Peter Koepke, Mathematical Logic Quarterly 62(3), 225-231 (2016)

Inter-locus as well as intra-locus heterogeneity in LINE-1 promoter methylation in common human cancers suggests selective demethylation pressure at specific CpGs, Nicole Nüsgen, Wolfgang Goering, Albertas Dauksa, Arijit Biswas, Muhammad Ahmer Jamil, Ioanna Dimitriou, Amit Sharma, Heike Singer, Rolf Fimmers, Holger Fröhlich, Johannes Oldenburg, Antanas Gulbinas, Wolfgang A Schulz, Osman El-Maarri, Clinical Epigenetics, 7(1):17 (2015)

The first measurable cardinal can be the first uncountable cardinal at any sucessor height , Arthur Apter, Ioanna Dimitriou, and Peter Koepke, Mathematical Logic Quarterly vol.60: 471-486 (2014)

Sets of good indiscernibles and Chang conjectures without choice , Ioanna Dimitriou, in Geschke, Löwe, Schlicht, eds., Infinity, Computability, and Metamathematics: Festschrift celebrating the 60th birthdays of Peter Koepke and Philip Welch, Templeton Press (Online) and College Publications, Tributes vol.23: 113–137 (2014)

Characterization of different courses of atopic dermatitis in adolescent and adult patients , Garmhausen D, Hagemann T, Bieber T, Dimitriou I, Fimmers R, Diepgen T, Novak N. Allergy vol.68(4): 498-506 (2013)

Symmetric Models, Singular Cardinal Patterns, and Indiscernibles , Ioanna M. Dimitriou, Bonn, Univ., Diss., 2011, URN:5N-27778

Inaccessible cardinals without the axiom of choice , Andreas Blass, Ioanna M. Dimitriou, and Benedikt Löwe Fundamenta Mathematicae vol.194: 179-189 (2007)

Strong limits and inaccessibility with non-wellorderable powersets , Ioanna M. Dimitriou, Master of Logic thesis. Supervisor: Dr.Benedikt Löwe. ILLC publication series MoL-2006-3

PDL for Ordered Trees , Loredana Afanasiev, Patrick Blackburn, Ioanna Dimitriou, Bertrand Gaiffe, Evan Goris, Maarten Marx, and Maarten de Rijke. Journal of Applied Non-Classical Logics 15(2): 115-135 (2005) b