Abstrakt. Denna uppsats visar hur man använder Girards intuitionistiska linjära logik utsträckt med en klassisk sublogisk till förnuft om pekarprogram. Mer specifikt, för det första, definierar tidningen bevisteorin för ILC (Intuitionistisk Linjär logik med Constraints) och visar att den är väldefinierad via ett bevis på skärning eliminering. För det andra, inspirerad av tidigare arbete av O'Hearn, Reynolds och Yang, förklarar tidningen hur man tolkar linjära logiska formler som beskrivningar av en programbutik. För det tredje definierar detta dokument ett enkelt obligatoriskt programmeringsspråk med muterbara referenser och matriser och ger kontrollvillkorsgenereringsregler som producerar påståenden i ILC. Slutligen identifierar vi ett fragment av ILC, ILC -, som är både decidable och stängd under generering av verifieringsförhållanden. Eftersom verifieringskonditionsgenereringen är syntaxstyrd, får vi ett decibelt förfarande för att kontrollera egenskaper hos pekarprogram.
Jia och Walker REF presenterar en intuitionistisk linjär logik med begränsningar som kombinerar logiken med en klassisk begränsningsdomän.
ILC: A foundation for automated reasoning about pointer programs
{'venue': 'In European Symposium on Programming Languages', 'journal': None, 'mag_field_of_study': ['Computer Science']}