Arve Gengelbach

dblp:229/4444 · DBLP profile ↗
← Back
3ranked-venue papers
2as first author
1since 2021 · last 2022
0000-0001-7708-348XORCID · verified

Domains — the database's venue-derived domains; a paper can count in several

Theory of computation · 3 · 2 first-author · 1 since 2021Artificial intelligence and machine learning · 1
YearPublicationVenuePosition
2022 A Verified Cyclicity Checker: For Theories with Overloaded Constants
Arve Gengelbach, Johannes Åman Pohjola
ITP1
2020 Proof-Theoretic Conservative Extension of HOL with Ad-hoc Overloading
Arve Gengelbach, Tjark Weber
ICTAC1
2020 A Mechanised Semantics for HOL with Ad-hoc Overloading
abstract
Isabelle/HOL augments classical higher-order logic with ad-hoc overloading of constant definitions— that is, one constant may have several definitions for non-overlapping types. In this paper, we present a mechanised proof that HOL with ad-hoc overloading is consistent. All our results have been formalised in the HOL4 theorem prover.
Johannes Åman Pohjola, Arve Gengelbach
LPAR2