-
es un editor de estructuras para la teoría de tipos monomórficos de Martin-Löf desarrollado en la Universidad de Chalmers . Es un predecesor de los asistentes de prueba Alfa , Agda , Cayenne y Coq y los lenguajes de programación tipificados de forma dependiente . Fue el primer lenguaje que admitió familias inductivas y coincidencia de patrones dependientes. -
Es un lenguaje de programación e interpretado usado habitualmente en el campo de la inteligencia artificial. -
Desarrollado por Fergus Henderson, Thomas Conway y Zoltan Somogyi.
Se basa en la lógica / funcional que combina; la claridad y la expresividad de la programación declarativa con funciones avanzadas de análisis estático y detección de errores.
