Hello, World!

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

Browse:

• about me
• software projects
• peer reviewed publications
• unpublished notes: TBA

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 very enthusiastic about lambda calculus and about 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 with Interstellar.
• I wrote the Choiceless Grapher almost from scratch, for my former colleagues in set theory.
• Since 2017 I'm working 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.
• I love all Lisps and every year I go to the European Lisp Symposium.

My favourite languages, vaguely ordered: Common Lisp, Scheme, 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.

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.

^calculus

A toy compiler of untyped lambda calculus into common lisp. I use ^, λ, and l, for lambda. Showcases representations of lambda terms in my quest to understand compilers.

• It closes open terms before compiling them.
• So far, showcased representations of lambda terms are:
  • the standard, single variable binding, parenthesised lambda terms as quoted common-lisp lists, e.g., '(^ x (x y))
  • de Bruijn representation (locally nameless for open terms), e.g., '(^ (0 y))
  • a (common) lisp representation, e.g., '(lambda (x) (funcall x y))
  • TBA: Implement Mogensen's continuation passing style self encoding of lambda calculus (Mogensen-Scott encoding).
  • TBA: Implement Tromp's
    • Combinatorial Logic representation in the form of SKI-calculus (towards a stack machine)
    • and his binary format for closed terms
• I provide transformations between these representations.
• There is a compiler to common-lisp, with simplifications currently only by closing open terms, fully beta-reducting in normal order with loop-catching, and then switching to common-lisp syntax and returning the resulting common-lisp closure.
• For the base I just followed Barendrecht and Barendsen's 1994 book "Introduction to Lambda Calculus" [Barendregt 1994]. TBA representations come with respective papers, which I am currently implementing.
• Tested:
  • By adding a catch-loop stepper-based reducer of the standard representation, I have been able to use cl-quickcheck on arbitrary generated terms, and quickcheck examples, theorems, and lemmas from [Barendregt 1994].
  • Standard, manually written tests are performed as well.
• Code tba

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 Spiffy 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 Spiffy 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