Agda hợp lý là Haskell đúng: Viết Haskell đã xác minh bằng cách sử dụng agda2hs
Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs.
Các ngôn ngữ được định kiểu phụ thuộc hiện đại như Agda có thể được sử dụng để thực thi tĩnh tính chính xác của các chương trình. Tuy nhiên, chúng vẫn thiếu hệ sinh thái lớn của một ngôn ngữ phổ biến hơn như Haskell. Để kết hợp sức mạnh của cả hai cách tiếp cận, các tác giả trình bày AGDA2HS, một công cụ dịch một tập hợp con biểu đạt của Agda thành Haskell có thể đọc được, xóa các kiểu phụ thuộc và bằng chứng trong quá trình này. Nhờ sự hỗ trợ của Agda cho các chú thích xóa, quá trình này vừa an toàn vừa minh bạch với người dùng. So với các công cụ khác để trích xuất chương trình, AGDA2HS sử dụng cú pháp đã quen thuộc với các lập trình viên chức năng, cho phép cả các cách tiếp cận bên trong và bên ngoài để xác minh và tạo ra mã Haskell dễ đọc và dễ kiểm tra bởi các lập trình viên không có kiến thức về Agda. Các tác giả trình bày một trường hợp sử dụng thực tế của AGDA2HS tại IOG để xác minh các thuộc tính của trình tạo chương trình. Mặc dù cả AGDA2HS và hệ sinh thái của nó vẫn còn mới, nhưng kinh nghiệm của các tác giả cho đến nay cho thấy đây là một cách tiếp cận khả thi để cung cấp lập trình hàm đã xác minh cho nhiều đối tượng hơn. Bài nghiên cứu này là một tập lệnh Agda có trình độ, do đó tất cả mã được kết xuất (Agda) đã được kiểm tra kiểu.