Coq: The World's Best Macro Assembler? (2013) [pdf]
Исследователи формализовали подмножество архитектуры x86 в Coq, сделав его "лучшим макро-ассемблером". Используя dependent types, type classes и notation, они упростили барочную семантику x86 до компактной формы. Биты, байты и память моделируются конкретными функциями, вычислимыми в Coq; они маппятся на математические объекты SSREFLECT (натуралы, целые по модулю 2^n). Ассемблер поддерживает привычный синтаксис (как в MASM), включая лексически-ограниченные метки, и генерирует hex-байты. Обычные определения Coq служат макросами для условных операторов, циклов, локальных переменных и процедур с параметрами. Доказана теорема корректности, связывающая машинный код с формулой separation logic для верификации.
Пример — код вычисления факториалов 10 (3628800) и 12 (479001600) с выводом через printf из MSVCRT.DLL. Макросы вроде call_cdecl3 (для cdecl-вызова), while и letproc скрывают детали. Ассемблируется в hex: EB 1A B8 01 00 00 00.... Coq генерирует PE-файл "winfact.exe" для Windows, исполняемый нативно. Поддержка bare metal возможна.