David Wang



I like logic and interactive theorem proving because I like to really understand something from the basics. It also feels good to be certain of things, even after you have forgotten the details of how you came to that conclusion.

This lead me to my current research area and the topic formal reasoning about GOLOG programs. It combines formal logic, programming language semantics, formal verification, and AI planning.

Research Experience

PhD research in Computer Science

October 2023 - ongoing

Researching formal reasoning about GOLOG programs under the supervision of Dr Mohammad Abdulaziz . GOLOG is a high-level agent modelling language meant to capture human intuition and common-sense reasoning in dynamic situations. The research aims to formalise GOLOG's semantics using techniques applied to programming languages as well as the situation calculus within the Isabelle/HOL theorem prover. It combines various applications of logic, from philosophy to AI.

Bachelor of Science - Final Year Project

September 2022 - April 2023

King's College London

London, United Kingdom

Regular Expressions, Lexing, Derivatives


Computer Science Research MPhil/PhD

October 2023 - ongoing

Bachelor of Science with Honours in Computer Science

September 2019 - July 2023

King's College London

London, United Kingdom

IB Diploma

September 2012 - July 2019

Vienna International School

Vienna, Austria


NMES Faculty Studentship

October 2023 - ongoing

A studentship for the duration of my studies as postgraduate research student at King's College London.


I did a few internships from summer 2021 to 2022.



Java, Scala, Kotlin, TypeScript

Interactive Theorem Proving:


Additional Information

The source code for this site can be found on GitHub.