Bahasa pemrograman - Mengenal Bahasa Pemrograman Agda

Mengenal Bahasa Pemrograman Agda

Pengertian Bahasa Pemrograman Agda

Agda adalah bahasa pemrograman fungsional tipe dependen yang awalnya dikembangkan oleh Ulf Norell di Chalmers University of Technology dengan implementasi yang dijelaskan dalam tesis PhD-nya. Sistem Agda asli dikembangkan di Chalmers oleh Catarina Coquand pada tahun 1999. Versi saat ini, awalnya dikenal sebagai Agda 2, adalah penulisan ulang penuh, yang harus dianggap sebagai bahasa baru yang memiliki nama dan tradisi yang sama.

Sejarah Bahasa Pemrograman Agda

Sistem yang didasarkan pada kerangka kerja Martin-Löf dan versi intens dari teori tipe Martin-Löf telah dikembangkan di Gothenburg sejak sekitar tahun 1990. Yang pertama disebut ALF (A Logical Framework). Pemeriksa tipe ditulis oleh Thierry Coquand dan antarmuka jendela ditulis oleh Lennart Augutsson berdasarkan ide-ide Bengt Nordström untuk merancang “editor bukti” untuk teori tipe Martin-Löf, di mana pengguna membuat bukti dengan menunjuk dan mengklik. Versi kedua dari ALF ditulis oleh Lena Magnusson. Pada tahun 2004 Kelompok Pemrograman Logika mulai berkolaborasi dengan Pusat Verifikasi dan Semantik di AIST di Amagasaki dalam pengembangan dan penerapan Agda. Pada saat ini, Pertemuan Implementasi Agda (AIM) dimulai dengan pertemuan dua tahunan bergantian antara Swedia dan Jepang. Pada tahun 2005 pekerjaan dimulai pada Agda versi baru, dan sebuah prototipe bernama AgdaLight ditulis oleh Ulf Norell dan Andreas Abel. Segera setelah itu pekerjaan pada desain dan implementasi sistem Agda saat ini (“Agda 2”) dimulai. Referensi utama adalah tesis Ulf Norell.

Contoh Kode Bahasa Pemrograman Agda

Compiler Bahasa Pemrograman Agda

  • Backend GHC = Menerjemahkan program Agda ke dalam program GHC Haskell.

LEAVE A REPLY

Please enter your comment!
Please enter your name here