Universidade do Minho  

Mapa do Site
Category theory on a computer - the example of the Coq system

While category theory is widely accepted for semantic analyses of programming languages, the use of formalised category theory is not widespread in computer science. Formalisations do exist in systems such as Mizar, Isabelle/HOL and NuPRL, but our focus is on the interactive programming and theorem-proving environment Coq, where formalisations by Saïbi/Huet and Simpson exist but are still not used for applications in computer science. An effort will be made to understand why this is so and to point to possible solutions. The mathematical problem is that of size and the additional computer-science problem that of equality of morphisms.
  © 2024 Universidade do Minho  - Termos Legais  - actualizado por CMAT Símbolo de Acessibilidade na Web D.