Universidade do Minho  

           
 
  Autenticação/Login
 
Contacts
Site Map
   
  print
 
back 
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.
 
back 
 
  © 2024 Universidade do Minho  - Legal Terms  - updated by CMAT Símbolo de Acessibilidade na Web D.