Constrained Higher-Order Rewriting and Program Equivalence (CHORPE)

Tijdsduur
2021 tot 2026
Projecttype
Onderzoek
Organisatieonderdeel
Software Science

CHORPE zal de theorie van gebonden termherschrijving aanzienlijk uitbreiden, en dit theoretisch kader gebruiken om de stand van zaken op het gebied van gelijkwaardigheidsanalyse van programma's te verbeteren. Dit bouwt voort op recente vorderingen van verschillende internationale onderzoeksgroepen, maar innoveert door nieuw gebruik van hogere-orde term herschrijving.

Term rewriting is een formeel systeem dat kan worden gebruikt om algoritmen te specificeren. Dankzij de eenvoudige en strikte definitie is het zeer geschikt voor formele analyse, en als gevolg zijn de eigenschappen ervan goed onderzocht. Hogere-orde termherschrijving omvat verder anonieme functies en lambda-binders. Dit maakt een zeer liberale categorie van systemen mogelijk, die een eenvoudige formele basis behoudt.

Recente studies suggereren dat methoden uit termherschrijving een krachtig hulpmiddel bieden voor diverse deelgebieden van programma-analyse. Programma's in talen als C, Java en Haskell kunnen worden vertaald in logically constrained term rewriting systems (LCTRSs). Dit biedt zowel een analysetaal op hoog niveau - waardoor dezelfde technieken beschikbaar komen in alle programmeertalen - als toegang tot inzichten uit een andere gemeenschap, ondersteund door tientallen jaren fundamenteel onderzoek. CHORPE wil verder gaan door beperkte herschrijving van hogere-orde termen te overwegen. Hogere-orde redeneren is een natuurlijke match voor objectgeoriënteerde en functionele talen en vermijdt veel intrinsieke beperkingen van eerder werk.

Het project tracht hogere-orde LCTRSs te vestigen als een standaard voor zowel herschrijving als programma-equivalentie, door twee verschillende maar met elkaar verweven onderzoeksrichtingen te volgen. Ten eerste zullen we een sterke theoretische basis leggen voor hogere-orde constrained rewriting met verschillende cruciale analysetechnieken. Ten tweede zullen we een krachtige methodologie voor programma-equivalentie ontwikkelen door programma's in traditionele talen te vertalen naar hogere-orde LCTRSs, en op herschrijving gebaseerde methoden te gebruiken om ze te analyseren. Alle resultaten zullen worden geïmplementeerd in een open-source analyse-instrument.

Project website

 

Contactinformatie