Supervised Students

Supervised Master Thesis

• Reconstructing Propositional Proofs in Type Theory
  Jonathan Prieto-Cubides
  Master in Applied Mathematics. Mathematical Sciences Department. Universidad EAFIT. 2017. [ pdf, slides, code ( Athena, Agda-Metis, Agda-Prop )]

  Abstract: We describe a syntactical proof-reconstruction approach to verify derivations generated by Metis prover to theorems in classical propositional logic. To verify such derivations, we formalise in type theory each inference rule of the Metis reasoning. We developed a tool jointly with two Agda libraries to translate Metis derivations to Agda proof-terms. These developments allowed us to type-check with Agda, Metis derivations step-by-step.

• Una formalización del sistema de los números reales (A Formalisation of the Real Numbers System)
  Jorge Ohel Acevedo Acosta and Jose Luis Echeverri Jurado
  Maestría en Matemáticas Aplicadas. Departamento de Ciencias Matemáticas. Universidad EAFIT. 2017. [ pdf for on-screen viewing, pdf for printing, slides, code ]

• Máquinas de Turing paraconsistentes: Algunas posibles definiciones y consecuencias (Paraconsistent Turing machines)
  Juan Carlos Agudelo Agudelo
  Tesis de especialización en Lógica y Filosofía. Departamento de Humanidades. Universidad EAFIT. 2003. [ ps ]

• Computabilidad de las redes neuronales recurrentes análogas (Computability of Analog Recurrent Neural Networks)
  Juan Carlos Agudelo Agudelo
  Maestría en Ingeniería Informática. Departamento de Informática y Sistemas (Master's thesis). Universidad EAFIT. 2001. [ tar.gz ]

Supervised Bachelors Thesis

• Category Theory Applied to Functional Programming
  Juan Pedro Villa Isaza
  Monografía Ingeniería de Sistemas (B.Sc. thesis). Universidad EAFIT. 2014. Mención de honor. [ pdf for on-screen viewing, pdf for printing, slides, code ]

  Abstract: We study some of the applications of category theory to functional programming, particularly in the context of the Haskell functional programming language, and the Agda dependently typed functional programming language and proof assistant. More specifically, we describe and explain the concepts of category theory needed for conceptualizing and better understanding algebraic data types and folds, functors, monads, and parametrically polymorphic functions. With this purpose, we give a detailed account of categories, functors and endofunctors, natural transformations, monads and Kleisli triples, algebras and initial algebras over endofunctors, among others. In addition, we explore all of these concepts from the standpoints of categories and programming in Haskell, and, in some cases, Agda. In other words, we examine functional programming through category theory.

• Factorización cuántica de números enteros: Una introspectiva al algoritmo de Shor (Shor's algorithm )
  Luis Moreno
  Monografía Ingeniería de Sistemas (B.Sc. thesis). Universidad EAFIT. 2004. Mención de honor. [ tar.gz ]

• Tipologías para problemas no Turing-computables (Taxonomy of Turing-incomputable problems)
  Carlos Arturo Pérez Monsalve
  Monografía Ingeniería de Sistemas (B.Sc. thesis) Universidad EAFIT. Mención de honor. [ tar.gz ]

• Lógicas paraconsistentes: Una introducción (Introduction to paraconsistent logics)
  José Luis Montes Gutiérrez and Camilo Ernesto Restrepo Ramírez
  Monografía Ingeniería de Sistemas (B.Sc. thesis). Universidad EAFIT. 2002. [ pdf ]

Supervised Research Practises

• A Set Theory Formalisation
  Alejandro Calle-Saldarriaga
  Práctica investigativa 1. Ingeniería Matemática. Universidad EAFIT. Semestre 2017–1. [ url ]

• Proof Reconstruction: Parsing Proofs
  Alejandro Gómez-Londoño
  Práctica investigativa 1. Ingeniería Matemática. Universidad EAFIT. Semestre 2015–1. [ url ]

• Proof Reconstruction: Parsing Proofs
  Diego Alejandro Montoya-Zapata
  Práctica investigativa 1. Ingeniería Matemática. Universidad EAFIT. Semestre 2015–1. [ url ]

• Formalisation of Programs with Positive Inductive Types
  Elisabet Lobo-Vesga
  Práctica investigativa 3. Ingeniería Matemática. Universidad EAFIT. Semestre 2014–1. [ url ]

• Hacia la formalización del razonamiento ecuacional sobre mónadas
  Elisabet Lobo Vesga
  Práctica investigativa 2. Ingeniería Matemática. Universidad EAFIT. Semestre 2013–1. [ url ]

• Teoría de categorías aplicada a la programación funcional con Agda
  Juan Pedro Villa-Isaza
  Práctica investigativa 1. Ingeniería Matemática. Universidad EAFIT. Semestre 2011–2. [ url ]

Andrés Sicard Ramírez Last modified: Tue Jun 7 11:14:51 -05 2022