Commit a4b419c2 authored by Ioanna M. Dimitriou H.'s avatar Ioanna M. Dimitriou H. 💬

First commit

parents
(defsystem "ioa.re"
:components ((:file "server"))
:depends-on ("hunchentoot"
"html-template"))
with import <nixpkgs> { };
stdenv.mkDerivation ({
name = "ioa.re";
buildInputs = [ ccl openssl ];
LD_LIBRARY_PATH = lib.makeLibraryPath [ openssl ];
})
[Unit]
Description=ioa's website
[Service]
ExecStart=/run/current-system/sw/bin/nix-shell %h/quicklisp/local-projects/ioa.re/start-ioa.sh
Restart=always
[Install]
WantedBy=default.target
\ No newline at end of file
(defpackage :ioa.re
(:use :cl :hunchentoot :html-template)
(:documentation "Creates ioa's website with html-template served by hunchentoot."))
(in-package :ioa.re)
;; Server and initial dispatch table
(defvar *server*)
(defvar *local-directory*
(namestring (asdf:system-source-directory :ioa.re)))
(defun local (rel-path)
(concatenate 'string *local-directory* rel-path))
(setq hunchentoot:*dispatch-table* ; dispatches folders, files, and pages
(list
(hunchentoot:create-static-file-dispatcher-and-handler
"/ioa.css" (local "www/ioa.css"))
(hunchentoot:create-prefix-dispatcher
"/" 'generate-index-page)))
(defun start-website (&key (address "localhost") (port 8383))
(setq *server* (hunchentoot:start
(make-instance 'easy-acceptor
:address address
:port port))))
(defun stop-website ()
(stop *server*))
(setq html-template:*default-template-pathname*
(concatenate 'string *local-directory* "www/templates/"))
;; ## Index page
(defun generate-index-page ()
(with-output-to-string (stream)
(html-template:fill-and-print-template
#P"ioa.tmpl"
'()
:stream stream)))
;;; debugging
(defun debug-mode-on ()
(setq *catch-errors-p* NIL)
(setq *show-lisp-errors-p* T))
(defun debug-mode-off ()
(setq *catch-errors-p* T)
(setq *show-lisp-errors-p* NIL))
(ql:quickload "ioa.re")
(in-package :ioa.re)
(start-website :address "127.0.0.1" :port 7878)
(loop do
(sleep 3600)
(room t))
#! /usr/bin/env nix-shell
#! nix-shell -i sh /home/ioa/quicklisp/local-projects/ioa.re/ioa.re.nix
# is the above nix-shell being replaced by
# /run/current-system/sw/bin/nix-shell in the systemd-config
# invoked call? In a way, it must know its name.
exec ccl -b -l ~/quicklisp/local-projects/ioa.re/start-ioa.lisp
html {
font-family: sans-serif;
}
b {
font-weight: 500;
}
a:link {
color: green;
}
div.info {
font-size: 1em;
line-height: .85em;
margin: 2em 4em 4em 2em;
width:100%;
float: right;
text-align: right;
}
div.info b {
font-weight: 900;
}
nav {
font-size: 1em;
font-weight: 900;
line-height: .85em;
position: fixed;
top: 0em;
width: 100%;
padding: 0.27em;
background-color: white;
}
nav ul {
list-style-type: none;
margin: 0;
padding: 0;
white-space: nowrap;
}
nav li{
display: inline-block;
margin: 0em 1em 0em 0em;
}
section.bit {
clear: both;
max-width: 40em;
margin: auto;
margin-bottom: 4em;
text-align: justify;
}
section.bit h1, section.bit h2, section.bit p {
padding: 0 0.5em;
margin-top: 0;
}
section.bit h1 {
padding-top: 1em;
}
section.bit h2 {
font-weight: 900;
font-size: 1em;
margin-top: 1em;
margin-bottom: 0.5em;
padding-top: 2em;
}
<section class="bit">
<a id="about"></a>
<h1 class="issue">about me</h1>
<p>
Short version:
</p>
<p>
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.
</p>
<p>
In some more detail:
<ul>
<li>Grew up in Thessaloniki, where I studied mathematics.</li>
<li>Did my master's degree in logic in Amsterdam.</li>
<li>Finished my Dr.rer.nat. degree in set theory in 2011 in Bonn, where I live now.</li>
<li>Afterwards I worked in medical statistics at the university clinic of Bonn, where I decided I like programming more.</li>
<li>Then I joined a project in formal mathematics and automated reasoning in ML and OCaml. You can see me talk about this <a href="https://www.youtube.com/watch?v=tfakmWsYq5g" target="_blank">on youtube</a> during <a href="http://fomus.weebly.com/" target="_blank">FOMUS</a>.</li>
<li>For many years until 2017, I taught and tutored mathematics to bachelors and masters students and to school kids.</li>
<li>I'm a software engineer, and a Common Lisper since 2014 with <a href="https://inters.co">Inters</a>tellar.</li>
<li>I wrote the <a href="https://cgraph.inters.co" target="_blank">Choiceless Grapher</a> almost from scratch, for my former colleagues in set theory.</li>
<li>Since 2017 I'm working on search engines (ELK), containers, docker, kubernetes, AWS, and openshift, as well as some Python AI projects.</li>
<li>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.</li>
<li>I love all Lisps and every year I go to the <a href="https://www.european-lisp-symposium.org/" target="_blank"> European Lisp Symposium</a>.</li>
</ul>
</p>
<p>
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).
</p>
<p>
I speak four human languages: Greek, English, German, Spanish, and I can still understand some Dutch.
</p>
</section>
<div class="info">
<b>Dr. Ioanna Matilde</b> <br>
<b>Dimitriou Henr&iacute;quez</b> <br>
dimitriou<span style="display:none">fnord</span>@ioa.re<br>
freenode.org: ioa<br>
<b>Software, Logic, Lisp</b><br>
</div>
<section class="bit">
<a id="index"></a>
<h1 class="issue">hello, world!</h1>
<p>I'm Ioanna, a software engineer in Bonn. Welcome to my homepage.</p>
<p>Browse:
<ul>
<li><a href="#about">about me</a></li>
<li><a href="#projects">software projects</a></li>
<li><a href="#publications">peer reviewed publications</a></li>
<li>unpublished notes: TBA</li>
</ul>
</section>
<!DOCTYPE html>
<html>
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>ioa's website</title>
<link rel="stylesheet" href="/ioa.css">
</head>
<header>
<!-- TMPL_INCLUDE 'menu.tmpl' -->
</header>
<!-- TMPL_INCLUDE 'header.tmpl' -->
<article>
<!-- TMPL_INCLUDE 'index.tmpl' -->
<!-- TMPL_INCLUDE 'about.tmpl' -->
<!-- TMPL_INCLUDE 'projects.tmpl' -->
<!-- TMPL_INCLUDE 'publications.tmpl' -->
<section>
<p>
<b>TBA: unpublished notes</b><br>
<br>
For the moment see <a href="https://web.archive.org/web/20161013235654/http://boolesrings.org/ioanna/">a cached version of my previous website</a>.
</p>
</section>
</article>
</html>
<div class="row">
<nav>
<ul>
<li><a href="#">home</a></li>
<li><a href="#about">about</a></li>
<li><a href="#projects">projects</a></li>
<li><a href="#publications">publications</a></li>
</ul>
</nav>
</div> <!-- / row -->
<section class="bit">
<h1 class="issue" id="projects">software projects</h1>
<p>
An incomplete list of my software projects. For my logic and for my statistics projects see <a href="#publications">publications</a>.
</p>
<h2>lambda</h2>
<p>
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.
</p>
<ul>
<li>Features a User Interface (UI) which includes:
<ul>
<li>A basic REPL "λ.base", which allows you to input λ terms which use the following symbols as primitives: <tt>:ID :TRUE :FALSE :S :AND :OR :IF :Y :OMEGA</tt></li>
<li>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: <tt>:A+ :A* :Aexp :Azero? :A+1 :A-1 :A-factorial</tt>, for plus, times, exponent, zero test, successor, predecessor, and factorial.</li>
<li>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.</li>
</ul></li>
<li>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.</li>
<li>For more features and more details see the <a href="https://gitlab.common-lisp.net/idimitriou/lambda/blob/master/README.md" target="_blank" >README</a> and the comments in the code. </li>
<li>Code <a href="https://gitlab.common-lisp.net/idimitriou/lambda" target="_blank">https://gitlab.common-lisp.net/idimitriou/lambda</a></li>
</ul>
<h2>cgraph.inters.co</h2>
<p>
A diagram maker for relationships between certain axioms of set theory.
<ul>
<li>Try it: <a href="https://cgraph.inters.co" target="_blank">https://cgraph.inters.co</a>.</li>
<li>See the source code: <a href="https://gitlab.common-lisp.net/idimitriou/jeffrey" target="_blank">https://gitlab.common-lisp.net/idimitriou/jeffrey</a></li>
<li>There are descriptions in the links above, and three detailed articles on Cgraph will appear as notes.</li>
</ul>
</p>
<h2>asd-graph</h2>
<p>
Dependency grapher for Common Lisp projects.
<ul>
<li>Graphs the dependencies between files and modules defined in an <code>.asd</code> file.</li>
<li>TBA: Graphing the dependencies and exported functions in packages defined in a <code>packages.lisp</code> file.</li>
<li>Description, source code and installation instructions:
<a href="https://gitlab.common-lisp.net/idimitriou/asd-graph" target="_blank">https://gitlab.common-lisp.net/idimitriou/asd-graph</a></li>
<li>In the <code>shiny-R</code> branch, you can deploy a Shiny server, using R, which serves a website with a file-form input, which when given an <code>.asd</code> file with a system definition, dynamically graphs that system. In Shiny R because it creates dynamic websites and because I love R, too.</li>
</ul>
</p>
<h2>nbg-hol</h2>
<p>
Group project:<br>
With the mathematical logic group of Bonn, that is Prof. Koepke and 11 bachelors and masters students doing
a <a href="http://www.math.uni-bonn.de/ag/logik/teaching/2015WS/praktikum_mathematische_logik.shtml" target="_blank">formal mathematics internship</a>,
we did a formalisation of von Neumann-Bernays-Gödel Set Theory of classes in Isabelle.
<ul>
<li>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.</li>
<li>We used the <a href="http://isabelle.in.tum.de/Isar/" target="_blank">Isar</a> proving language, which makes formal proving very accecible to beginners.</li>
<li>You can see me present this project <a href="https://www.youtube.com/watch?v=tfakmWsYq5g" target="_blank">on youtube</a> during <a href="http://fomus.weebly.com/" target="_blank">FOMUS</a>, where I spent a lovely week talking with category and type theorists, who are pleasantly quite direct about their opinions.</li>
</ul>
</p>
<h2>my repositories</h2>
<p> For more software projects take a look here:
<ul>
<li>Common-lisp projects: <a href="https://gitlab.common-lisp.net/idimitriou" target="_blank">https://gitlab.common-lisp.net/idimitriou</a></li>
<li>All projects: <a href="https://github.com/ioannad" target="_blank">https://github.com/ioannad</a></li>
</ul>
</p>
</section>
<section class="bit">
<h1 class="issue" id="publications">peer-reviewed publications</h1>
<!--
<p>
<b>Set theory has the same strength as second-order arithmetic with regularity properties</b>,
Ioanna Dimitriou, Peter Koepke, Regula Krapf, and Michael Möllerfeld
<i>Submitted</i>
</p>
-->
<p>
<a href="http://faculty.baruch.cuny.edu/aapter/papers/adk15.pdf" target="_blank">
<b>All uncountable cardinals in the Gitik model are almost Ramsey and carry Rowbottom filters</b>,
</a>
Arthur Apter, Ioanna Dimitriou, and Peter Koepke,
<i>Mathematical Logic Quarterly 62(3), 225-231 (2016)</i>
</p>
<p>
<a href="http://www.ncbi.nlm.nih.gov/pubmed/25798207" target="_blank">
<b>Inter-locus as well as intra-locus heterogeneity in LINE-1 promoter methylation in common human cancers suggests selective demethylation pressure at specific CpGs</b>,
</a>
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,
<i>Clinical Epigenetics, 7(1):17 (2015)</i>
</p>
<p>
<a href="http://faculty.baruch.cuny.edu/aapter/papers/adk14.pdf" target="_blank">
<b>The first measurable cardinal can be the first uncountable cardinal at any sucessor height</b>
</a>,
Arthur Apter, Ioanna Dimitriou, and Peter Koepke,
<i>Mathematical Logic Quarterly vol.60: 471-486 (2014)</i>
</p>
<p>
<a href="https://pdfs.semanticscholar.org/3f9c/1c7e0b7741726bab1348edfe0f08b712bff8.pdf" target="_blank">
<b>Sets of good indiscernibles and Chang conjectures without choice</b>
</a>,
Ioanna Dimitriou,
<i>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&#8211;137 (2014)</i>
</p>
<p>
<a href="http://www.ncbi.nlm.nih.gov/pubmed/23452057" target="_blank">
<b>Characterization of different courses of atopic dermatitis in adolescent and adult patients</b>
</a>,
Garmhausen D, Hagemann T, Bieber T, Dimitriou I, Fimmers R, Diepgen T, Novak N.
<i>Allergy vol.68(4): 498-506 (2013)</i>
</p>
<p>
<a href="http://hss.ulb.uni-bonn.de/2012/2777/2777.pdf" target="_blank">
<b>Symmetric Models, Singular Cardinal Patterns, and Indiscernibles</b>
</a>,
Ioanna M. Dimitriou,
<i>Bonn, Univ., Diss., 2011, URN:5N-27778</i>
</p>
<p>
<a href="http://www.illc.uva.nl/Research/Publications/Reports/PP-2006-46.text.pdf" target="_blank">
<b>Inaccessible cardinals without the axiom of choice</b>
</a>,
Andreas Blass, Ioanna M. Dimitriou, and Benedikt Löwe
<i>Fundamenta Mathematicae vol.194: 179-189 (2007)</i>
</p>
<p>
<a href="http://www.illc.uva.nl/Publications/ResearchReports/MoL-2006-03.text.pdf" target="_blank">
<b>Strong limits and inaccessibility with non-wellorderable powersets</b>
</a>,
Ioanna M. Dimitriou,
<i>Master of Logic thesis. Supervisor: Dr.Benedikt Löwe. ILLC publication series MoL-2006-3</i>
</p>
<p>
<a href="https://staff.fnwi.uva.nl/m.derijke/wp-content/papercite-data/pdf/afanasiev-pdl-2005.pdf" target="_blank">
<b>PDL for Ordered Trees</b>
</a>,
Loredana Afanasiev, Patrick Blackburn, Ioanna Dimitriou, Bertrand Gaiffe, Evan Goris, Maarten Marx, and Maarten de Rijke.
<i>Journal of Applied Non-Classical Logics 15(2): 115-135 (2005)</i>
b </p>
</section>
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment