{"id":27072,"date":"2026-10-06T03:00:34","date_gmt":"2026-10-06T01:00:34","guid":{"rendered":"https:\/\/www.proefschriftmaken.nl\/portfolio\/kasper-hagens\/"},"modified":"2026-10-31T11:36:19","modified_gmt":"2026-10-31T10:36:19","slug":"kasper-hagens","status":"publish","type":"us_portfolio","link":"https:\/\/www.proefschriftmaken.nl\/en\/portfolio\/kasper-hagens\/","title":{"rendered":"Kasper Hagens"},"content":{"rendered":"","protected":false},"featured_media":27073,"template":"","meta":{"_acf_changed":false},"university_us_portfolio":[17],"class_list":["post-27072","us_portfolio","type-us_portfolio","status-publish","has-post-thumbnail","hentry","university_us_portfolio-radboud-universiteit"],"acf":{"main_text":"","naam_van_het_proefschift":"Rewriting Induction for Higher-Order Constrained Rewriting","samenvatting":"Het garanderen dat software zich gedraagt zoals bedoeld is een centrale uitdaging in softwareontwikkeling. Formele verificatie biedt wiskundig rigoureuze methoden om te redeneren over computer code. Een van deze methoden is termherschrijven, waarbij de elementaire rekenstappen van een programma worden gespecificeerd door een verzameling herschrijfregels en het corresponderende computationele gedrag wordt vastgelegd via de herschrijfrelatie. Deze herschrijfrelatie kan worden opgevat als een taalonafhankelijke operationele semantiek, die uitermate geschikt is voor het defini\u00ebren van methoden voor programma-analyse, zoals terminatie- en complexiteitsanalyse. Een tekortkoming van traditionele herschrijfsystemen is echter dat primitieve datastructuren, zoals integers, inductief gecodeerd moeten worden. Deze benadering correspondeert niet met de manier waarop dergelijke datastructuren worden verwerkt in programmeertalen. Een oplossing wordt geboden door Logically Constrained Simply-typed Term Rewriting Systems (LCSTRSs), waarin primitieve datastructuren semantisch kunnen worden gemodelleerd.\n\nIn deze thesis gebruiken we de hogere-orde uitbreiding van LCTRSs, genaamd Logically Constrained Simply-typed Term Rewriting Systems (LCSTRSs), om program equivalence te bestuderen. De herschrijf relatie wordt gebruikt om een notie van equivalentie te defini\u00ebren, gebaseerd op de intu\u00eftie dat twee programma\u2019s equivalent zijn indien zij hetzelfde input-outputgedrag vertonen. We ontwikkelen verschillende bewijssystemen om program equivalence in praktijk te kunnen vaststellen. Al deze systemen zijn gebaseerd op welgefundeerde inductie over term herschrijf systemen, die als methode afhankelijk is van terminatie, dat dus een belangrijke rol zal spelen in deze thesis.\n\nEen van de redenen om een bewijssysteem te willen hebben is het mogelijk maken van equivalentiebewijzen via de computer. Hoewel program equivalence in het algemeen onbeslisbaar is (dus complete bewijs-automatisering is niet mogelijk), introduceren we heuristieken om in eenvoudigere gevallen een zekere mate van automatisering te realiseren. Daarnaast is een substantieel deel van de thesis gericht op ground confluence. Deze eigenschap is noodzakelijk om de correctheid van de methode voor het weerleggen van program equivalence te garanderen, maar is ook op zichzelf een belangrijke eigenschap: in een terminerend en ground confluent term herschrijf systeem berekent reductie in wezen een uniek resultaat voor elke grondterm. We ontwikkelen een methode om ground confluence van LCSTRSs te bewijzen, en als onderdeel hiervan defini\u00ebren we kritieke paren voor LCSTRSs.","summary":"Ensuring that software behaves as intended is a central challenge in software development. Formal verification provides mathematically rigorous methods for reasoning about programming code. One such method is term rewriting, in which the elementary computational steps defining a program are specified by a set of rewrite rules and the corresponding program behavior is captured by the rewrite relation. The rewrite relation can be seen as a language-independent operational semantics, suitable for defining methods for program analysis, such as termination and complexity analysis. However, a limitation of traditional term rewriting systems is that primitive data structures, such as integers, must be encoded inductively. This does not correspond to the way such data structures are treated in real programming languages. A solution is provided by Logically Constrained Term Rewriting Systems (LCTRSs), where primitive data structures can be treated semantically, thereby providing a more faithful basis for reasoning about program behavior.\n\nIn this thesis, we use the higher-order extension of LCTRSs, called Logically Constrained Simply-typed Term Rewriting Systems (LCSTRSs), to study program equivalence. The rewrite relation is used to define a notion of program equivalence, based on the intuition that two programs are equivalent if they exhibit the same input-output behavior. We develop several proof systems to establish program equivalence in practice. All of them are based on well-founded induction over term rewriting systems, which in turn relies on termination, which will therefore play an important role in this thesis.\n\nOne of the reasons for wanting to have a proof system is to enable computer-guided equivalence proofs. Although program equivalence is undecidable in general (i.e. complete proof automation is not possible), we introduce heuristics to realize a certain degree of automation in simple cases. A substantial part of the thesis is centered around ground confluence. This property is necessary to guarantee the correctness of the method for disproving program equivalence, but it is also important in its own right: in a terminating and ground-confluent system, reduction essentially computes a unique result for every ground term. We develop a method for proving ground confluence of LCSTRSs, and as part of this, we define critical pairs for LCSTRSs.","auteur":"Kasper Hagens","auteur_slug":"kasper-hagens","publicatiedatum":"8 december 2026","taal":"EN","url_flipbook":"https:\/\/ebook.proefschriftmaken.nl\/ebook\/kasperhagens?iframe=true","url_download_pdf":"https:\/\/ebook.proefschriftmaken.nl\/download\/7ba898cb-83c6-40af-a2a0-4c07def6c4b7\/highres","url_epub":"","ordernummer":"19637","isbn":"9789465153155","doi_nummer":"10.54195\/9789465153155","naam_universiteit":"Radboud Universiteit","afbeeldingen":27073,"video_url":"","podcast_url":"","naam_student:":"","binnenwerk":"","universiteit":"Radboud Universiteit","cover":"","afwerking":"","cover_afwerking":"","design":""},"_links":{"self":[{"href":"https:\/\/www.proefschriftmaken.nl\/en\/wp-json\/wp\/v2\/us_portfolio\/27072","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.proefschriftmaken.nl\/en\/wp-json\/wp\/v2\/us_portfolio"}],"about":[{"href":"https:\/\/www.proefschriftmaken.nl\/en\/wp-json\/wp\/v2\/types\/us_portfolio"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.proefschriftmaken.nl\/en\/wp-json\/wp\/v2\/media\/27073"}],"wp:attachment":[{"href":"https:\/\/www.proefschriftmaken.nl\/en\/wp-json\/wp\/v2\/media?parent=27072"}],"wp:term":[{"taxonomy":"university_us_portfolio","embeddable":true,"href":"https:\/\/www.proefschriftmaken.nl\/en\/wp-json\/wp\/v2\/university_us_portfolio?post=27072"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}