ALF ("Otro marco lógico") 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 . [1] [2]