Georgios V. Pitsiladis

(he/him)

PhD in Mathematical Logic in Computer Science, with research on formal methods, formalised mathematics, and other applications of logic.
Interested in all aspects of software, from day-to-day coding (as type-safely as possible) to abstract logical and mathematical reasoning.
Passionate about free (as in freedom) software.
Based in Greece

Profile picture

Publications

Journal Papers

  1. Georgios V. Pitsiladis & Costas D. Koutras: Embedding the Calendar and Time Type System in Temporal Type Theory, Journal of Applied Non-Classical Logics 35(2)
  2. Georgios V. Pitsiladis & Petros S. Stefaneas: A logical framework to model software development by multiple agents following a common specification, Journal of Logic and Computation 34(5)
  3. Costas D. Koutras & Georgios V. Pitsiladis: Galois connections for bilattices, Algebra universalis 82 (full text)

Conference Papers

  1. Georgios V. Pitsiladis & Petros S. Stefaneas: Converting BPMN Diagrams to Privacy Calculus, Eighth Symposium on Working Formal Methods (FROM 2024), Electronic Proceedings in Theoretical Computer Science (code, slides)
  2. Georgios V. Pitsiladis & Petros S. Stefaneas: Implementation of Privacy Calculus and Its Type Checking in Maude, ISoLA 2018: Leveraging Applications of Formal Methods, Verification and Validation. Verification, Springer International Publishing (slides, Maude code, Maude example)

Theses

  1. On logical methods for specifications: abstract and type-theoretic approaches, PhD, Department of Mathematics, School of Applied Mathematical and Physical Science, National Technical University of Athens, Greece. Supervised by Petros S. Stefaneas, co-supervised by Costas D. Koutras.
  2. Notions of Galois connections for Bilattices, MSc in Alogithms, Logic, and Discrete Mathematics, National and Kapodistrian University of Athens & National Technical University of Athens, Greece. Supervised by Costas D. Koutras, co-supervised by Petros S. Stefaneas.
  3. Type checking privacy policies in the π-calculus and an executable implementation in Maude, Diploma (integrated master) of Applied Mathematics, National Technical University of Athens, Greece. Supervised by Petros S. Stefaneas

Translations

  1. Διακριτά Μαθηματικά με εφαρμογές (978-960-418-994-6) translation from English to Greek of Handbook of discrete and combinatorial mathematics, 2nd edition (978-1-58488-780-5) (I was responsible for translating chapters 7–14 of the Greek version & the biographies)

Selected talks

  1. Using the Theory of Institutions for Semiotic–Argumentational Treatment of Mathematical Proof, International Conference on Mathematical and Computational Linguistics for Proofs. (slides, video)
  2. Embedding the Calendar and Time Type System in Temporal Type Theory, Hellenic-Romanian Logic and Computation Seminar. (slides)
  3. Pre-bilattices in Univalent Foundations, 28th International Conference on Types for Proofs and Programs (TYPES 2022), University of Nantes. (slides, video)
  4. A relativistic formal description of software development, 7th World Congress and School on Universal Logic (UNILOG 2022), Orthodox Academy of Crete. (slides)
  5. Privacy Calculus in Maude, Workshop "Rules: Logic and Applications", National Technical University of Athens. (slides)
  6. Type Checking Conditional Purpose‐Based Privacy Policies in the π‐calculus & Implementing Type Checking of π‐calculus Processes for Privacy in Maude, Formal Methods on Privacy, Limassol, Cyprus. (slides)

Teaching

Teaching assistant

  1. Graph theory (exercises grading), School of Applied Mathematical and Physical Science, National Technical University of Athens
  2. Introduction to object oriented programming (labs & exercises grading), School of Applied Mathematical and Physical Science, National Technical University of Athens
  3. Discrete mathematics (exercises), School of Applied Mathematical and Physical Science, National Technical University of Athens