I am a Postdoctoral researcher in the Trustfull project at EECS at KTH Royal Institute of Technology in Stockholm, Sweden. In 2021 I earned a PhD degree in Computer Science at Uppsala University, adviced by Tjark Weber. My research interests include formal verification and interactive theorem proving applied to problems within computer security.
In previous work I study properties of higher-order logic with ad-hoc overloading, and contribute to the CakeML Project and the HOL4 theorem prover.
@inproceedings{GengelbachA22,
author = {Gengelbach, Arve and {\AA}man Pohjola, Johannes},
title = {{A Verified Cyclicity Checker:
For Theories with Overloaded Constants}},
booktitle = {13th International Conference on Interactive Theorem Proving
(ITP 2022)},
pages = {15:1--15:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16724},
URN = {urn:nbn:de:0030-drops-167240},
doi = {10.4230/LIPIcs.ITP.2022.15},
}@techreport{GengelbachA21,
author = {Arve Gengelbach and Johannes {{\AA}man Pohjola}},
title = {{Towards Correctly Checking for Cycles in Overloaded Definitions}},
institution = {Department of Information Technology, Uppsala University},
department = {Division of Computing Science},
year = {2021},
number = {2021-001},
month = mar,
issn = {1404-3203},
url = {http://www.it.uu.se/research/publications/reports/2021-001/},
biburl = {http://www.it.uu.se/research/publications/reports/2021-001/bibtex-2021-001.bib},
pages = {14}
}@inproceedings{GengelbachAW20,
author = {Arve Gengelbach and
Johannes {{\AA}man Pohjola} and Tjark Weber},
year = {2021},
title = {{Mechanisation of Model-theoretic Conservative Extension
for HOL with Ad-hoc Overloading}},
editor = {Claudio Sacerdoti Coen and Alwen Tiu},
booktitle = {Proceedings Fifteenth Workshop on Logical Frameworks and
Meta-Languages: Theory and Practice, Paris, France, 29th June
2020},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {332},
publisher = {Open Publishing Association},
pages = {1-17},
issn = {2075-2180},
doi = {10.4204/EPTCS.332.1},
url = {http://eptcs.org/content.cgi?LFMTP2020},
biburl = {https://cgi.cse.unsw.edu.au/~eptcs/bibtex.cgi?332.1}
}@inproceedings{DBLP:conf/ictac/GengelbachW20,
author = {Arve Gengelbach and Tjark Weber},
title = {{Proof-theoretic Conservativity for HOL with Ad-hoc
Overloading}},
booktitle = {Theoretical Aspects of Computing - {ICTAC} 2020 - 17th
International Colloquium, Macau, China, November 30 - December 4,
2020, Proceedings},
editor = {Violet Ka I Pun and Volker Stolz and
Adenilso da Silva Sim{\~{a}}o},
series = {Lecture Notes in Computer Science},
volume = {12545},
pages = {23--42},
year = {2020},
publisher = {Springer},
isbn = {978-3-030-64276-1},
url = {https://doi.org/10.1007/978-3-030-64276-1_2},
doi = {10.1007/978-3-030-64276-1_2},
timestamp = {Tue, 01 Dec 2020 09:11:53 +0100},
biburl = {https://dblp.org/rec/conf/ictac/GengelbachW20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}@inproceedings{LPAR23:MechanisedSemanticsforHOL,
author = {Johannes {{\AA}man Pohjola} and Arve Gengelbach},
title = {{A Mechanised Semantics for HOL with Ad-hoc Overloading}},
booktitle = {LPAR23. LPAR-23: 23rd International Conference on Logic for
Programming, Artificial Intelligence and Reasoning},
editor = {Elvira Albert and Laura Kov{\'{a}}cs},
series = {EPiC Series in Computing},
volume = {73},
pages = {498--515},
year = {2020},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/9Hcd},
doi = {10.29007/413d}
}@inproceedings{DBLP:journals/entcs/GengelbachW18,
author = {Arve Gengelbach and
Tjark Weber},
editor = {Sandra Alves and
Renata Wasserman},
title = {{Model-Theoretic Conservative Extension for Definitional
Theories}},
booktitle = {12th Workshop on Logical and Semantic Frameworks, with
Applications, {LSFA} 2017, Bras{\'{\i}}lia, Brazil,
September 23-24, 2017},
series = {Electronic Notes in Theoretical Computer Science},
volume = {338},
pages = {133--145},
publisher = {Elsevier},
year = {2017},
month = {Sep},
url = {https://doi.org/10.1016/j.entcs.2018.10.009},
doi = {10.1016/j.entcs.2018.10.009},
timestamp = {Wed, 05 Feb 2020 13:49:05 +0100},
biburl = {https://dblp.org/rec/journals/entcs/GengelbachW18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@phdthesis{Gengelbach21,
author = {Arve Gengelbach},
institution = {Department of Information Technology, Uppsala University},
pages = {34},
school = {Uppsala University},
title = {Conservative Definitions for Higher-order Logic with Ad-hoc
Overloading},
series = {Digital Comprehensive Summaries of Uppsala Dissertations from
the Faculty of Science and Technology},
ISSN = {1651-6214},
number = {2021},
ISBN = {978-91-513-1150-0},
year = {2021},
URL = {https://urn.kb.se/resolve?urn=urn%3Anbn%3Ase%3Auu%3Adiva-435841}
}Together with a colleague I run Uppsala Cryptoparty.
Guide for git repositories on the university’s servers
Resources for the HOL4 Theorem Prover
Scooping the Loop Snooper – A poetic proof that the Halting Problem is undecidable, by Geoffrey K. Pullum
This game represents the untyped lambda calculus. A hungry alligator is a lambda abstraction, an old alligator is parentheses, and eggs are variables. The eating rule corresponds to beta-reduction. The color rule corresponds to (over-cautious) alpha-conversion. The old age rule says that if a pair of parentheses contains a single term, the parentheses can be removed.
This is a personal webpage. More information.