Thế giới cú pháp an toàn về kiểu và phạm vi với ràng buộc: ngữ nghĩa và bằng chứng
A type- and scope-safe universe of syntaxes with binding: their semantics and proofs.
Cú pháp của hầu hết mọi ngôn ngữ lập trình đều bao gồm khái niệm về biến ràng buộc (Binder) và các lần xuất hiện ràng buộc tương ứng, cùng với các khái niệm đi kèm về tính tương đương α, phép thay thế tránh giữ lại, kiểu ngữ cảnh, môi trường Runtime, v.v. Trước đây, việc triển khai và lập luận về ngôn ngữ lập trình đòi hỏi phải xử lý cẩn thận để duy trì hành vi đúng của các biến bị ràng buộc. Các ngôn ngữ lập trình hiện đại bao gồm các tính năng cho phép các ràng buộc như phạm vi an toàn được thể hiện trong các kiểu. Tuy nhiên, lập trình viên vẫn buộc phải viết lại cùng một mẫu chuẩn cho mỗi lần triển khai mới của một thao tác an toàn phạm vi (ví dụ: phép đổi tên, phép thay thế, lược bỏ, printing) và sau đó viết lại để chứng minh tính chính xác. Các tác giả trình bày một thế giới biểu thức cú pháp với ràng buộc và chứng minh cách (1) triển khai các phép duyệt an toàn phạm vi một lần và mãi mãi bằng lập trình tổng quát; và (2) cách suy ra các thuộc tính của các phép duyệt này bằng chứng minh tổng quát. Mô tả thế giới, các phép duyệt và chứng minh tổng quát, cũng như các ví dụ của các tác giả đều đã được chính thức hóa trong Agda và có sẵn trong tài liệu đi kèm có sẵn trực tuyến tại https://github.com/gallais/generic-syntax.