ALF ("Otro marco lógico") es un editor de estructuras para la teoría de tipos monomórficos Martin-Löf desarrollada en la Universidad de Chalmers . Es un predecesor de los asistentes de prueba Alfa , Agda , Cayenne y Coq y de los lenguajes de programación de tipo dependiente . Fue el primer idioma que apoyó a las familias inductivas y la coincidencia de patrones dependientes . [1] [2]
Referencias
- ^ Thierry Coquand (1992). "Coincidencia de patrones con tipos dependientes" . En Bengt Nordström , Kent Petersson y Gordon Plotkin (editores), Actas electrónicas del tercer taller anual de BRA sobre marcos lógicos (Båstad, Suecia) .
- ^ Thorsten Altenkirch , Conor McBride y James McKinna (2005). "Por qué son importantes los tipos dependientes" .
Otras lecturas
- Lena Magnusson y Bengt Nordström . "El editor de pruebas ALF y su motor de pruebas" .
- Thorsten Altenkirch , Veronica Gaspes, Bengt Nordström y Björn von Sydow. "Una guía del usuario de ALF" .