I detta dokument presenteras GMETA: ett generiskt ramverk för första ordningens representationer av variabel bindning som en gång för alla tillhandahåller många av de så kallade infrastrukturlemmas och definitioner som krävs vid mekaniseringar av formell metateori. Ramverket använder datatyp-generisk programmering och modulära programmeringstekniker för att tillhandahålla ett universum som representerar en familj av datatyper. Detta universum är generiskt på två olika sätt: det är språk-generiskt i den meningen att flera objektspråk kan representeras inom universum; och det är representation-generiskt, vilket innebär att det är parameteriserbart över det särskilda valet av första ordningen representationer för bindemedel (till exempel lokalt namnlös eller de Bruijn). Med hjälp av detta universum genomförs flera bibliotek som tillhandahåller allmän infrastruktur lemmas och definitioner. Dessa bibliotek används i fallstudier baserade på POPLmark utmaningen, som visar att hantering av utmanande bindningskonstruktioner, som de som finns i System F <:, är möjligt med GMETA. All GMETA:s allmänna infrastruktur genomförs i Coq-teoretikern, vilket säkerställer att denna infrastruktur är sund. På grund av GMETA:s modulära design kan biblioteken dessutom enkelt användas, utökas och anpassas av slutanvändarna.
I REF, Lee et al. Använda generisk programmeringsteknik för att utveckla mekaniseringar av formell metateori i Coq-proofassistenten.
A Generic Formal Metatheory Framework for First-Order Representations
{'venue': 'ESOP', 'journal': None, 'mag_field_of_study': ['Computer Science']}