Articulo de referencia

ALF (asistente de pruebas)

ALF ("Another logical framework") es un editor de estructuras para la teoría de tipos monomórfica de Martin-Löf desarrollado en la Universidad de Chalmers . Es un predecesor de ...

ALF ("Another logical framework") es un editor de estructuras para la teoría de tipos monomórfica de Martin-Löf desarrollado en la Universidad de Chalmers . Es un predecesor de los asistentes de prueba Alfa , Agda , Cayenne y Rocq , así como de lenguajes de programación con tipado dependiente . Fue el primer lenguaje en admitir familias inductivas y coincidencia de patrones dependientes . [ 1 ] [ 2 ]

Referencias

  1. 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) .
  2. Thorsten Altenkirch , Conor McBride y James McKinna (2005). "Por qué importan los tipos dependientes" .

Lecturas adicionales

  • 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" .
  • Esparto