Arve Gengelbach

Hej, I am a PhD student in the group for theory of concurrent systems at Uppsala University. My principal supervisor is Tjark Weber.

In my research I am interested in interactive theorem proving and formal verification, in particular I am studying properties of higher-order logic with ad-hoc overloading and contributing to and using the CakeML Project and the HOL4 theorem prover.

My contact details

Publications

  1. A. Gengelbach and J. Åman Pohjola.
    Towards Correctly Checking for Cycles in Overloaded Definitions (Technical report).
    bibtex
    @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}
    }
  2. A. Gengelbach, J. Åman Pohjola and T. Weber.
    Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading. Post-proceedings of LFMTP 2020. Details on the mechanisation. Slides.
    bibtex
    @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}
    }
  3. A. Gengelbach and T. Weber.
    Proof-theoretic Conservative Extension for HOL with Ad-hoc Overloading. ICTAC 2020. Slides.
    bibtex
    @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}
    }
  4. A. Gengelbach and T. Weber.
    Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading (Extended abstract). LFMTP 2020.
  5. J. Åman Pohjola and A. Gengelbach.
    A Mechanised Semantics for HOL with Ad-hoc Overloading. LPAR23.
    bibtex
    @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}
    }
  6. A. Gengelbach and T. Weber.
    Model-theoretic Conservative Extension of Definitional Theories. LSFA 2017
    bibtex
    @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}
    }

Theses

Teaching

Miscellaneous