¡Hola a todas! Bienvenidas al foro de discusión sobre Coq en español.
Cómo ya bien sabréis, Coq es un software para la realización de demostraciones asistidas por ordenador. El equipo de desarrollo de Coq os desea muchos momentos de diversión y aprendizaje con esta maravillosa herramienta que ya ha cumplido más de 35 años de historia.
Esta parte del foro en español, o castellano, está dedicada a todas y todos aquellos que quieran hablar y preguntar sobre Coq, y se sientan más cómodos usando este nuestro idioma.
No hay una temática concreta para el subforo, cualquier tipo de pregunta o comentario es bienvenido; no obstante no está demás recordar que, como es norma en el mundo de la investigación, las discusiones de alto contenido técnico tienden a ocurrir en la parte angloparlante del foro.
Las normas de convivencia del foro se rigen por el código de conducta general del projecto Coq. Se pueden resumir de una manera muy sencilla, intentemos divertirnos y respetar a todo el mundo.
Algunos datos sobre Coq:
- Coq fue creado sobre el año 1983 en el instituto de investigación francés I.N.R.I.A.
- Su nombre viene de coq “gallo” símbolo nacional francés, y tiene relación con una cierta tradición de nombrar lenguages de programación tras animales.
- Coq ha sido utilizado para varios proyectos pioneros, por ejemplo el compilador verificado CompCert, o las demostraciones del “Teorema de los cuatro colores” y el “Teorema de Feit-Thompson”