PLCOMP Telegram 72
https://grosskurth.ca/bib/1997/cardelli.pdf
"Program Fragments, Linking, and Modularization" Luca Cardelli.

Статья поднимает вопрос корректности раздельной компиляции и линковки, и потому — я считаю — обязательна к прочтению для всех авторов языков программирования! 😃

Уже во введении на простейшем примере создания воображаемой программы, состоящей всего из двух модулей, разрабатываемых независимо, автор иллюстрирует, наверное, все проблемы, при этом возникающие. Между делом Карделли упоминает публичные репозитории артефактов (типа Maven Central или Nuget. Напомню, что статья опубликована в 1996 году!). Многие из обозначенных проблем линковки раздельно скомпилированных модулей до сих пор не решены ни в мейнстримных, ни в исследовательских языках.

В качестве основного результата Карделли предлагает, вероятно, первую формальную модель раздельной компиляции и последующей линковки, позволяющую строго рассмотреть вопрос о корректности этих процессов. Корректность в этом смысле приведённой простейшей системы модулей для просто типизированного лямбда-исчисления (в качестве модельного языка) формально доказывается. Автор, конечно же, указывает на необходимость расширения модели как в сторону более развитых языков (параметрический полиморфизм, ООП), так и в сторону более сложных систем модулей (параметризованные модули, "функторы" в духе Standard ML, первоклассные модули). Существуют ли такие работы, непосредственно продолжающие это исследование, мне не известно.

Однако, в качестве related work и дальнейшего чтения могу указать на работы по формализации (и доказательству корректности) раздельной компиляции для языка C в рамках проекта CompCert.

#separatecompilation #linking #modules #stlc



tgoop.com/plcomp/72
Create:
Last Update:

https://grosskurth.ca/bib/1997/cardelli.pdf
"Program Fragments, Linking, and Modularization" Luca Cardelli.

Статья поднимает вопрос корректности раздельной компиляции и линковки, и потому — я считаю — обязательна к прочтению для всех авторов языков программирования! 😃

Уже во введении на простейшем примере создания воображаемой программы, состоящей всего из двух модулей, разрабатываемых независимо, автор иллюстрирует, наверное, все проблемы, при этом возникающие. Между делом Карделли упоминает публичные репозитории артефактов (типа Maven Central или Nuget. Напомню, что статья опубликована в 1996 году!). Многие из обозначенных проблем линковки раздельно скомпилированных модулей до сих пор не решены ни в мейнстримных, ни в исследовательских языках.

В качестве основного результата Карделли предлагает, вероятно, первую формальную модель раздельной компиляции и последующей линковки, позволяющую строго рассмотреть вопрос о корректности этих процессов. Корректность в этом смысле приведённой простейшей системы модулей для просто типизированного лямбда-исчисления (в качестве модельного языка) формально доказывается. Автор, конечно же, указывает на необходимость расширения модели как в сторону более развитых языков (параметрический полиморфизм, ООП), так и в сторону более сложных систем модулей (параметризованные модули, "функторы" в духе Standard ML, первоклассные модули). Существуют ли такие работы, непосредственно продолжающие это исследование, мне не известно.

Однако, в качестве related work и дальнейшего чтения могу указать на работы по формализации (и доказательству корректности) раздельной компиляции для языка C в рамках проекта CompCert.

#separatecompilation #linking #modules #stlc

BY PLComp


Share with your friend now:
tgoop.com/plcomp/72

View MORE
Open in Telegram


Telegram News

Date: |

Channel login must contain 5-32 characters Add the logo from your device. Adjust the visible area of your image. Congratulations! Now your Telegram channel has a face Click “Save”.! Telegram desktop app: In the upper left corner, click the Menu icon (the one with three lines). Select “New Channel” from the drop-down menu. On June 7, Perekopsky met with Brazilian President Jair Bolsonaro, an avid user of the platform. According to the firm's VP, the main subject of the meeting was "freedom of expression." For crypto enthusiasts, there was the “gm” app, a self-described “meme app” which only allowed users to greet each other with “gm,” or “good morning,” a common acronym thrown around on Crypto Twitter and Discord. But the gm app was shut down back in September after a hacker reportedly gained access to user data.
from us


Telegram PLComp
FROM American