Omitir los comandos de cinta
Saltar al contenido principal
Inicio de sesión
Universidad EAFIT
Carrera 49 # 7 sur -50 Medellín Antioquia Colombia
Carrera 12 # 96-23, oficina 304 Bogotá Cundinamarca Colombia
(57)(4) 2619500

​​​​​​​​Logic and Computation Seminar

Discussion group: EAFIT: Log​ic and Computation (announces, discussion about the talks, etc.)
Anyone interested is welcome to attend!


Joint seminar Universidad de Antioquia/Universidad EAFIT

Dat​​​​e Talk​​
Speaker: Juan Carlos Agudelo-Agudelo

Affiliation: Professor, Departament of MathematicsUniversidad de Antioquia

Title: Towards a Paraconsistent Type Theory

Abstract:  In this talk, initially intuitionistic logic and intuitionistic type theory are described, then Nelson's paraconsistent logic is described and a "paraconsistent type theory" based on that logic is introduced.

Slides: [ pdf ]

Place: Universidad EAFIT, 38-108

Time: 2:00 p.m. - 4:00 p.m.

Speaker: Santiago Echeverri-Valencia

Affiliation: Master student in Mathematicas, Universidad de Antioquia

Title: Topological semantics for intuitionistic logic

Abstract: First, we present the natural deduction system (NJp) for Propositional Intuitionistic Logic (IL). Then, IL is characterized by means of a possible worlds semantics and it is shown that a subclasse of models named pointed models are enough to characterize IL. Finally,  we present a topological interpretation for IL and show soundness and completeness for this interpretation with the help of the possible worlds semantics previously presented.

Slides: [ pdf ] (Spanish)

Place: Universidad EAFIT, 35-502

Time: 2:00 p.m. - 4:00 p.m.

Speaker: Andrés Felipe Tamayo-Arango

Affiliation: Undergraduate student in Mathematical Engineering, Universidad EAFIT

Title: Formal Proof for Termination of Programs Using Ordinal Numbers

Abstract: Even though termination is an undecidable problem, there are some approaches for proving termination of programs. One of those are the ordinal numbers. In this regard, we present a short review of literature, showing fundamental ideas in the field of termination and ordinal numbers and then, via an example of a term rewrite system, we establish how to prove termination in this kind of systems using ordinal numbers.

Slides: [ pdf ]

Place: Universidad de Antioquia - sede Medellín, 5-105

Time: 3:00 p.m. - 4:00 p.m.

Speaker: Andrés Felipe Velásquez-Trujillo

Affiliation: Undergraduate student in Mathematics, Universidad de Antioquia

Title: Consistency of Arithmetic

Abstract: We present the theorems and tools necessary for demonstrating the consistency of Peano arithmetic, translating it into Heyting arithmetic by means of Gödel’s double-negation interpretation, subsequently translating Heyting arithmetic to Gödel’s system T, and using a notion of "realizability".

Slides: [ pdf ] (Spanish)
Place: Universidad de Antioquia - sede Medellín, 5-105
Time: 2:00 p.m. - 3:00 p.m.

Speaker: Juan Sebastían Cárdenas

Affiliation: Undergraduate student in Mathematical Engineering, Universidad EAFIT

Title: Representation of Ordinal Numbers

Abstract: Ordinal numbers have been studied since latest 19th century by different mathematicians. This numbers have been used in several different applications such as proving algorithm termination, theoretical Turing machines that surpass the undecidability barrier, proof theory and more. In this talk, different representations of ordinal numbers in different areas of mathematics are presented.

Slides: [ pdf ]
Place: Universidad de Antioquia - sede Oriente
Time: 3:00 p.m. - 4:00 p.m.

Speaker: Daniela Cartagena-Cartagena

Affiliation: Undergraduate student in Mathematics, Universidad de Antioquia

Title: Girard's Paradox

Abstract: In this talk, we briefly present the pure type systems $\lambda$U and $\lambda$U$^-$ as extensions of the system $\lambda$HOL, which allows to obtain the higher order logic with polymorphic domains and quantification over all types, respectively. Moreover, we show that these systems are inconsistent, and describe some of its consequences.

Slides: [ pdf ]
Place: Universidad de Antioquia - sede de Oriente

Time: 2:00 p.m. - 3:00 p.m.

Speaker: Andrés Sicard-Ramírez

Affiliation: Professor, Departament of Mathematical Sciences, Universidad EAFIT

Title: Introduction to Agda

Slides: N/A
Place: Universidad EAFIT, 23-204
Time: 2:00 p.m. - 4:00 p.m.


Dat​​​​e Talk​​
​​Speaker: Elisabet Lobo

Affiliation: PhD student, Chalmers University of Technology, Gothenburg, Sweden

Title: Interpreting Lambda Calculus via Category Theory (A pragmatic programming guide for the non-expert)

Abstract: The programming language Haskell is well-known for easily embedding domain-specific languages (EDSLs) via libraries. Many EDSLs are designed as tools to easily express programs in other platforms. The goal is to enjoy the features provided by the EDSLs and the host language (e.g., types, compositionality, etc.) in order to obtain well-behaved code in some low-level language. Such EDSLs are implemented in a deep embedded fashion in order to enable optimizations. Unfortunately, this kind of EDSLs sooner or later end up repeating the work of the host compiler. Recently, a new approach called Compiling to Categories [1] has emerged and promises to avoid such replication of work. It relies on understanding the categorical model of Cartesian Closed Categories (CCC). That means that, to use this new technique, it becomes necessary to understand basic category theory and CCC. Unfortunately, when learning about such topics and its relation to functional programs, one faces the risk of diving into mathematical books with difficult-to-penetrate notation, getting lost in abstract notions, and eventually giving up. Instead, this pearl aims to guide Haskell developers to the understanding of all of such abstract concepts via Haskell code. We present two EDSLs in Haskell: one for simply-typed lambda terms and another for CCC and show how to translate programs from one into the other---a well-known result [2]. We also show how to execute CCC programs via the categorical abstract machine (CAM). Moreover, we extend our implementation of simply-typed  lambda calculus with primitive operators, branching, and fix points via appropriate enhancements to our EDSL of CCC and CAM based on category theory concepts. All this journey is going to be grounded in Haskell code, so that developers can experiment and stop fearing such abstract concepts as we did.

[1] Conal Elliott. 2017. Compiling to categories. Proc. ACM Programing Languages 1, ICFP, Article 48 (Sept. 2017), 24 pages.

[2] Joachim Lambek. 1986. Cartesian Closed Categories and Typed Lambda-Calculi. In Proceedings of the Thirteenth Spring School of the LITP on Combinators and Functional Programming Languages. Springer-Verlag, 136–175.

This talk is based on a joint-work with Solène Mirliaz and Alejandro Russo.

Slides: N/A

Video: N/A

Place: 29-205
Time: 11:00 a.m. - 12:00 m.


Dat​​​​e Talk​​
2017-07-27​​​Speaker: Alejandro Calle-Saldarriaga

Affiliation: Undergraduate student in Mathematical Engineering, Universidad EAFIT

Talk title: A Set Theory Formalization

Abstract: Set theory has been is one of the most important fields for the foundations of mathematics, so having a formalization (i.e. a translation of its axiom and theorems into some proof assistant) is desirable. In this talk, we present a set theory formalization of the Z axioms and some theorems using Agda.

Slides: [ pdf ]
Place: 38-405
Time: 11:00 a.m. - 12:00 m.

2017-06-01Speaker: Jonathan Prieto-Cubides

Affiliation: Master student in Applied Mathematics, Universidad EAFIT

Talk title: The Simple Typed Lambda Calculus

Abstract: We present a formalization of the syntax in Agda for the Simple Typed Lambda Calculus (STLC) with some of its properties and a description of the typechecking for this type system.

Slides: [ pdf ]
Agda code: GitHub repository
Place: 38-501B
Time: 5:00 p.m. - 6:00 p.m.


Speakers: Jorge Acevedo-Acosta and José Echeverri-Jurado
Affiliation: Master students in Applied Mathematics, Universidad EAFIT

Talk title: Una formalización del sistema de los números reales

Abstract: En el campo del razonamiento automático se habla de la formalización de una teoría cuando sus teoremas son demostrados automáticamente o cuando sus demostraciones son verificadas por un asistente de pruebas. Se presenta una formalización de algunos aspectos del sistema de los números reales en el asistente de pruebas Agda. Se demuestran formalmente de forma interactiva y automática algunas propiedades del sistema. Las demostraciones automáticas fueron realizadas por demostradores automáticos de teoremas de propósito general para la lógica de predicados de primer orden.

​Slides: [ pdf ]
Agda code: GitHub repository​
Place: 38-306
Time: 5:00 p.m. - 6:00 p.m.

2017-05-25Speaker: Camilo Andrés Rodríguez-Garzón

Affiliation: Master student in Applied Mathematics, Universidad EAFIT

Talk title: Braun Trees in Agda

Abstract: In this exposing it is analyze from a particular ambit the Braun trees in order to establish some concepts and definitions that enable a greater understanding about what is and means. It is expose a property and is explain some methods that have Braun trees.

Slides: [ pdf ]
Place: 38-501B
Time: 5:00 p.m. - 6:00 p.m.


Speaker: Jonathan Prieto-Cubides
 Master student in Applied Mathematics, Universidad EAFIT

Talk title: Proof Reconstruction in Classical Propositional Logic

Abstract: In order to type-check proofs in Agda found by Metis Prover to problems in First-Order Logic, we present in this opportunity our progress first with Classic Propositional Logic, making an overview of the proof reconstruction workflow and our recent developments.

Slides:pdf ]
Place: 38-306
Time: 2:00 p.m. - 3:00 p.m.


Speaker: Andreas Abel
Affiliation: Senior Lecturer, Chalmers University of Technology, Gothenburg, Sweden

Talk title: Normalization by Evaluation

Abstract: In computer systems that manipulate syntactic objects, like computeralgebra systems, compilers, and theorem provers, we find algorithms that check whether two expressions are equal.  Some expression classes admit normal forms.  For objects of these classes, equality can be decided by checking that the expressions under cons​ideration have the same normal form. Conversion to normal form is called normalization.

In this talk, I show how normalizers can be obtained from interpreters in a principled and elegant way.  The process of normalizing an expression via an interpreter is called normalization by evaluation. I will demonstrate normalization by evaluation for two structures: monoids and lambda-calculus.

Normalization by evaluation is applied in type-directed partial evaluation of functional programs, in implementation of proofassistants, and in foundational studies of Type Theory.

Slides: [ pdf ]
Video: [ link ]
Place: 27-302
Time: 2:00 p.m. - 3:00 p.m


Speaker: Alejandro Gomez-Londoño
Affiliation: ​Proof Engineer at Data61/CSIRO, Australia

Talk title: seL4: Formal verification of an OS kernel [1] (A proof engineer perspective)

Abstract: The seL4 microkernel is "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement" [2]. In this talk, we present a high-level overview of seL4s specification and proofs, along with user cases and future challenges of the seL4 project.

[1] seL4: F​ormal verification of an OS kernel​. Gerwin Klein et al, ACM Symposium on Operating Systems Principles 2009. 
[2] seL4 project website

Slides: [ pdf ]
Video: [ link ]


Speaker: Elisabet Lobo-Vesga
Affiliation: Mathematical Engineer, Universidad EAFIT

Talk title: (Perhaps Less Simple) Monadic Equational Reasoning

Slides: [ pdf ]


Date​​ T​alk


Speaker: Jonathan Prieto-Cubides
Affiliation: Master student in Applied Mathematics, Universidad EAFIT

Talk title: Kripke Semantics

Abstract: In this talk, we briefly get in touch with the ideas of Kripke semantics. That is one of the semantics for non-classic logic, in particular for intuitionistic logic. We will present some of the theory behind its formalism and finally we expect to show the same formalism in Agda.

Slides: [ pdf ]


Speaker: Camilo Andrés Rodríguez-Garzón
Affiliation: Master student in Applied Mathematics, Universidad EAFIT

Talk title: A Brief Introduction to Program Analysis

Abstract: In this exposition, we analyze from a general ambit, the area of Program Analysis in order to establish some concepts and definitions that enable a greater understanding of what is and means. We present some applications and two main branches of Programs Analysis. Some techniques widely used are Control-flow, Data-flow Analysis, Abstract Interpretation, Type System and Effect System for Analysis of Static. For Dynamic Programs Analysis, we present Testing Programs, Monitoring and Programs Slicing. At the end, we give an example exposing common tools used for analyzing programs.

Slides: [ pdf ]


Speaker: Alejandro Calle-Saldarriaga
Affiliation: Undergraduate student in Mathematical Engineering, Universidad EAFIT

Talk title: A non-learning premise selection algorithm for Apia

Abstract: Automatic theorem provers need to recieve a reasonably small number of premises in order for them to be able to prove a given conjecture with limited processor time. In large theories this is not always possible, as many irrelevant clauses are added to the premises. In order to solve this problem, premise selection algorithms have emerged in the past few years, some using non-learning methods and others using learning ones. Our goal in this project is to implement a non-learning premise selection algorithm for Apia, in order to further link the interactive theorem prover Agda with Authomatic theorem provers.

Slides: [ pdf ]


Speaker: Jonathan Prieto-Cubides
Affiliation: Master student in Applied Mathematics, Universidad EAFIT

Talk title: OnlineATPs. A client for the TPTP

Abstract: OnlineATPs is a Haskell program open source for connects to the web service SystemOnTPTP of the TPTP World.This new tool allows us to use ATPs without installing any of them. We can install it on Linux, Windows or Mac. With OnlineATPs we are capable to test a problem against at least sixty ATPs, check for unsatisfability, get some proofs and others functions.

Slides: [ pdf​ ]


Date T​al​k


Speaker: Danny Arlen de Jesus Gómez Ramírez

Talk title: Towards the Classification of the Metagenerators of Mathematical Theories: Formal Conceptual Blending

Abstract: During the last decades of research in cognitive sciences several fundamental cognitive abilities of the human's mind has been found and has been formalized, such as analogy and case base reasoning, methaphor and conceptual blending. We use an specific formalization of the last one, described in terms of colimits of formal concepts defined in many-sorted first order logic, in order to meta-generate the most fundamental concepts of fields theory as a formal conceptual blending of five fundamental concepts. The implementation uses the software HETS within the Common Algebraic Specification Language (CASL).


Speaker: Elisabet Lobo-Vesga

Talk title: [Overview] Two can keep a secret if one of them uses Haskell

Abstract: As an attendant to ICFP 2015, I learned about formal and applied aspects of Functional Programming. For me, one of the most relevant research was "Functional Pearl: Two Can Keep a Secret, If One of Them Uses Haskell" by Alejandro Russo where he introduces an interesting and a simple application of Functional Programming in Information Flow field.


Speakers: Jorge Acevedo-Acosta and José Echeverri-Jurado

Talk title: Real Numbers Formalization: Completeness Axiom and Automatic Reasoning

Abstract: We present the formalization of the completeness axiom in the proof assistant Agda and additionally the use of ATPs to prove different properties of real numbers.

Slides: [ pdf ]


Speaker: Alejandro Gómez Londoño

Talk title: Overview of ICFP 2015

Slides: [ pdf ]


Speakers: Jorge Acevedo-Acosta and José Echeverri-Jurado

Talk title: Field and Order Axioms of Real Numbers in Agda

Abstract: The introduction of the real numbers can be done in different ways. In this talk, from an axiomatic construction, we formalize the real numbers and some of their properties in the proof assistant Agda.

Slides: [ pdf ]


Speaker: Mauricio Toro-Bermúdez

Talk title: Process Ordering in a Process Calculus for Spatially-Explicit Ecological Models

Abstract: We will present an extension of PALPS, a process calculus proposed for the spatially-explicit individual-based modeling of ecological systems, with the notion of a policy. A policy is an entity for specifying orderings between the different activities within a system. It is defined externally to a PALPS model as a partial order which prescribes the precedence order between the activities of the individu- als of which the model is comprised. The motivation for introducing policies is twofold: one the one hand, policies can help to reduce the state-space of a model; on the other hand, they are useful for exploring the behavior of an ecosystem under different assumptions on the ordering of events within the system. To take account of policies, we refine the semantics of PALPS via a transition relation which prunes away executions that do not respect the defined policy. Furthermore, we propose a translation of PALPS into the probabilistic model checker PRISM . We illustrate our framework by applying PRISM on PALPS models with policies for conducting simulation and reachability analysis.


A. Philippou, M. Toro-Bermúdez and Margarita Antonaki. PALPS: A process calculus for spatially-explicit ecological models. Scientific Annals of Computer Science, 23(1):119--167, 2013.

A. Philippou and M. Toro-Bermúdez. Process ordering in a process calculus for spatially-explicit ecological models. In Proc. of MokMasd '13, Madrid, Spain, September, 2013. Volume 8368 of Lecture Notes in Computer Science, pages 345--361, Springer July 2013.

Mauricio Toro, Anna Philippou, Christina Kassara, Spyros Sfenthourakis: Synchronous Parallel Composition in a Process Calculus for Ecological Models. ICTAC 2014: 424-441.

Slides: [ pdf ]


Speaker: Elisabet Lobo-Vesga

Talk title: Formalization of Programs with Positive Inductive Types

Abstract: Most of proof assistants only work with strictly positive types, then verification of programs that use positive (and negative) types is uncommon. We use the programming logic created by Bove, Dybjer and Sicard-Ramírez that accept positive types to formalize the termination of a breadth-first search in a binary tree that uses a positive data type.

Slides: [ pdf​ ]


Da​te ​Talk


Speaker: Alejandro Gómez-Londoño

Talk title: Mostly functional does not work

Abstract: Based on a recent paper of Erik Meijer, we explore the drawbacks of adding functional features into imperative languages as a way to solve the challenges arising from fields like concurrency and parallelism, and suggest a more fundamentalist approach as a better solution.

Slides: [ pdf ]


Speaker: José Ignacio Serna-Naranjo

Talk title: Clean – Uniqueness Typing

Abstract: Clean is a functional programming language that shares many features with Haskell, but one big difference is the use of uniqueness typing. We will present the key properties of the language and the concept of uniqueness typing in the context of Clean.

Slides: [ pdf ]


Speaker: Elisabet Lobo-Vesga

Talk title: Type Classes in Coq

Abstract: Coq is a proof assistant that provide a formal language to write mathematical definitions and theorems. It also can automatically extract from Coq specifications to OCaml or Haskell source code. We present the implementation of Haskell type classes in Coq after a short introduction to the system.

Slides: [ pdf ]


Speaker: Alejandro Gómez-Londoño

Talk title: Idris: A Language with Dependent Types

Abstract: Idris is a general purpose pure functional programming language with dependent types, suitable for both theorem proving and programming in general. We will present the key features of Idris as well as practical examples using the REPL in Emacs.

Slides: [ pdf​ ]


Da​t​e Talk


Speaker: Juan Pedro Villa-Isaza

Talk title: Enoch: Just Enoch

Abstract: We explore algebras over endofunctors and their relation to algebraic data types in Haskell.


Speaker: Santiago Palacio-Gómez

Talk title: Curry: Integrating logic and functional paradigms

Abstract: Curry is a programming language designed to join the most important concepts from declarative programming paradigms. It combines features from functional programming (nested expressions, lazy evaluation, high-order functions, etc.) and logic programming (logic variables, built-in search, etc.). We are going to explore some main concepts from the language that highlight aspects from both paradigms.

Slides: [ pdf ]


Speaker: Juan Francisco Cardona-McCormick

Talk title: Research Subjects


Speaker: Diego Echeverri-Saldarriaga

Talk title: Why Erlang Matters (For the Social Games Industry)

Abstract: We have heard before that Erlang is a fault-tolerant, functional language with an actor model on top. But who uses it? How does it behave in production systems? How does it compare to other languages like Ruby? The idea of this talk is not only provide some answers to these questions, but also give a good picture of the patterns used, and the libraries we use to support some of the most popular social games.

Slides: [ .zip ]


Speaker: Andrés Sicard-Ramírez

Talk title: Research Subjects


Speaker: Néstor Cataño-Collazos

Talk title: Research Subjects


Speaker: Andrés Sicard-Ramírez

Talk title: Combining Interactive and Automatic Proofs in First-Order Theories (research proposal - 2014)

Abstract: We shall show our research proposal for 2014. I would appreciate your feedback.

Slides: [ pdf ]


Speaker: Andrés Sicard-Ramírez

Talk title: Consistency of a Programming Logic for a Version of PCF Using Domain Theory

Abstract: After showing some required concepts and theorems we establish the consistency of a programming logic for a type-free version of a core functional programming language---Plotkin's PCF language---through the existence of a domain model.

Slides: [ pdf ]


Speaker: Juan Pedro Villa-Isaza

Talk title: Enoch: Not the father of Methuselah

Abstract: We explore mathematical monads and their relation to monads in Haskell and Agda.


Speaker: Juan Pedro Villa-Isaza

Talk title: Enoch: The father of Irad

Abstract: We explore natural transformations and their relation to polymorphic functions in Haskell and Agda.


Speaker: Alejandro Gómez-Londoño

Talk title: An Introduction to Erlang

Abstract: An overview of the history and some basic functional and concurrent concepts of Erlang.

Slides: [ pdf ]


Speaker: Juan Pedro Villa-Isaza

Talk title: Enoch: A son of Cain

Abstract: We explore mathematical functors and their relation to functors in Haskell and Agda.


Speaker: John Jairo Silva

Talk title: Implementation of syntax and semantic of grammars through parser combinators and attribute grammars

Abstract: The structure of programming language is defined with syntax and semantic rules and its mining with different types of semantic. In this conference we shall show the implementation of two programming language through the parser combinators to define its structure, and attribute grammars to define its meaning. Besides we shall show the advantages and problems that arise when defining operational semantics in both programming languages.

Slides: [ pdf ]



Date ​Talk


Speaker: Santiago Angée-Agudelo

Talk title: Yesod: A functional programming approach for developing web applications

Abstract: Functional programming languages have been historically pushed into the background regarding computer science areas such as web development. With the classic imperative approach for web development appears some significant problems like the difficulties of security threats, the stateless nature of HTTP, the multiple languages necessary to create a powerful web application, among others. A few years ago a handful of frameworks for developing web applications with Haskell have appeared. Yesod is a web development framework that attempts to ease the web development process by using the strengths of the Haskell programming language, making use of some of its features, including type safety, pattern matching on algebraic data types among others. By building upon Haskell, entire classes of bugs disappear. We are going to show through a simple application built in Yesod how a functional programming approach can solve some common problems that are constant features in the imperative programming frameworks for web development, and how a Haskell approach could simplify the process of web development.


Speaker: Elisabet Lobo-Vesga

Talk title: Reasoning about functional programs

Abstract: One of the greatest advantages of the pure functional languages is that they allow to use equational reasoning, therefore the depuration and verification of pure functional programs is easier. But this purity exclude the computational effects, by this reason the monadic functions, that encapsulate these effects and keep the purity, represent an important feature into the functional languages as Haskell. Nevertheless, due to the monads have imperative structure; it has not been possible to create an accepted approach for using the equational reasoning with them, if it would be possible, it would mean an important advance in the field of verification of programs. We will show the basic concepts and some examples for using equational reasoning on monadic programs.

Slides: [ pdf ]


Speaker: Federico Builes-Vásquez

Talk title: Functional Reactive Programming: Another Approach to Asynchronous Systems

Abstract: The interactions between users, software and systems with implied latency depend on changes in state and time that are hard to model due to their asynchronous nature. Today we mostly use CPS[0] programming to solve this problem, but if we are not extra careful with our code it can turn into what is known as "callback hell". In this talk we'll study the problems with the proliferation of callbacks, the similarities between "callback hell" and "goto hell"[1] and functional reactive programming (FRP) as a possible solution to these issues. 

[0] Gerald Jay Sussman and Guy L. Steele, Jr. "Scheme: An interpreter for extended lambda calculus". AI Memo 349: 19, December 1975.
[1] Edsger W. Dijkstra. Go To Statement Considered Harmful. Communications of the ACM, Vol. 11, No. 3, March 1968, pp. 147-148.

Slides: [ pdf ]


Speaker: Andrés Eugenio Castaño-Cardenas

Talk title: Abstract Interpretation


Speaker: Juan Francisco Cardona-McCormick

Talk title: Functional Fixpoint Evaluator for Partially Circular Attributes Grammars

Abstract: One of the possible semantics for circular attribute grammars is to assign a fixpoint value to circularly defined attributes. The main application of this interpretation is in program analysis. We present a method which generates such fixpoint evaluators for circular attribute grammars in the functional language Haskell. We start by identifying the parts of the grammar that contain a circular dependency and the parts that are guaranteed to be non-circular. From the latter we generate normal functional sub-evaluators, whereas for the former we generate iterating sub-evaluators. These sub-evaluators are combined to form a complete evaluator for the grammar. We show the strategies which can be taken to avoid unnecessary re-evaluations and discuss some of the trade-offs involved.


Speaker: Andrés Sicard-Ramírez

Talk title: Verification of Functional Programs. I. First-Order Theory of Combinators

Abstract: What if we have written a Haskell-like program and we want to verify it? What programming logic should we use? What proof assistant should we use? Can part of the job be automatic? In this talk, we propose the First-Order Theory of Combinators (FOTC) for answering the first question. Using FOTC we can deal with general recursion (structural, non-structural, nested and higher-order recursion), higher-order functions, partial and total correctness, and inductive and co-inductive predicates.

Slides: [ pdf ]


Da​te Talk


Speaker: Diego Echeverri-Saldarriaga

Talk title: Introduction to Uniplate

Abstract: This talk will introduce Uniplate, a Haskell library for generic traversals. In the first part I will show how the functions provided by Uniplate are used for "Scrapping the Boilerplate" in the context of a simple mathematical interpreter. The second part will show how Uniplate works and how can you create your own type-instances for your data structures.

Slides and code: [ .tar ]


Speaker: Adolfo León Builes-Jiménez

Talk title: GSoC Experience: working with Darcs and getting involve in an open source project

Abstract: During this talk I will be doing an introduction to the Google Summer of Code program, my experience as GSoC participant and Darcs.


Speaker: Juan Francisco Cardona-McCormick

Talk title: Functional Circular Fixed Point Evaluator for Attribute Grammars

Abstract: Attribute grammar is a formalism defined by Knuth (1968) used to define a semantic for a context free grammar. This formalism can only be used when a attribute grammar description is well-defined (when there is not exist a circular attribute dependency between some of them). Farrow (1986) defined a solution for some non well-defined attribute grammars, but this solution only cover for static imperative evaluators. In this talk, we show how to implement a functional circular fixed point evaluator for attribute grammars.


Speaker: Andrés Sicard-Ramírez

Talk title: Using automated and interactive theorem proving in Agda

Abstract: Interactive proof assistants based on higher-order logics (e.g. Agda, Coq) usually lack a good support of proof automation (even in the first-order world). We have been developing a tool in which Agda users obtain support from first-order automatic theorem provers (ATPs) such as Equinox and Eprover. In our current approach, the ATPs are called by our tool on users' marked conjectures after the Agda type-checking is finished.

Slides: [ pdf ]


Speaker: Diego Echeverri-Saldarriaga

Talk title: Simulating disfix operators

Abstract: Extensibility in programming language design is about the possibility of letting the programmer add it's own syntactic constructions. This property allows to transfer some built-in functions to libraries. This thesis shows some problems implementing a programming language with object oriented features starting from a lazy, functional language that uses a subset of disfix operators as an extensibility mechanism.


Speaker: Diego Echeverri-Saldarriaga

Talk title: Turing machines in Haskell

Abstract: In this talk we show a simple implementation of a Turing machine using Haskell. We show how easy is add error-handling, non-determinism, IO, and probabilistic behavior using monads.

Slides: [ .tgz ]


Speaker: Juan Carlos Agudelo-Agudelo

Talk title: Non-classical Logic Circuits

Abstract: The model of Boolean Circuits is generalized in order to allow the definition of circuits based on non-classical logics. The generalization is accomplished by considering the "Polynomial Ring Calculus", a new semantics and proof method adequate for many non-classical logics, including logics which can not be characterized by means of finite (truth-functional) matrices. Some properties concerning computational complexity are analyzed.

Slides: [ pdf ] and [ pdf ]


Speaker: Juan Carlos Agudelo-Agudelo

Talk title: Paraconsistent Turing Machines

Abstract: It is defined two models of "Paraconsistent Turing Machines", by axiomitizing classical Turing machines and substituting the underlying logic by different paraconsistent logics. It is proved hat the models obtained have different properties with respect to computational complexity, in this way it is showed that computational complexity can be viewed as logic-relative. Some connections with quantum computation are also pointed out.

Slides: [ pdf ]


D​ate Talk


Speaker: Juan Pedro Villa-Isaza

Talk title: Proofs = Programs

Abstract: From the Agda Wiki:

  • Agda is a dependently typed functional programming language. It is strongly typed and types may depend on elements in other types (like Vector i the type of vectors of length i). It has parameterized modules, mixfix operators, Unicode characters, and an interactive Emacs interface (the type checker can assist the programmer in writing the program)
  • Agda is a proof assistant. It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It has many similarities with other proof assistants based on dependent types, such as Coq, Epigram, Matita and NuPRL.

We give a gentle introduction to dependent types and functional programming using Agda as a dependently typed functional programming language and we explore the basic features of Agda using its interactive Emacs interface.


Speaker: Diego Echeverri-Saldarriaga

Talk title: Monads in .Net

Abstract: Monads have been used in Haskell as an abstraction for different kinds of computation. Nowadays lots of programmers are using monads in disguise just by using LINQ. We show how the monad mechanism can be used in C# and F# by translating different examples from the "All about monads" Haskell tutorial and also some advanced methods like Asynchronous Workflows.

Slides: [ .org ]


Speaker: Rafael David Rincón-Bermúdez

Talk title: CMMI and software process improvement

Abstract: Capability Maturity Model® Integration (CMMI) is a process improvement approach that provides organizations with the essential elements of effective processes. It can be used to guide process improvement across a project, a division, or an entire organization. CMMI helps integrate traditionally separate organizational functions, set process improvement goals and priorities, provide guidance for quality processes, and provide a point of reference for appraising current processes.

Slides: [ pdf​ ]


Speaker: Adolfo León Builes-Jiménez

Talk title: Combinator parsing

Abstract: There are numerous ways to implement a parser for a given syntax; using parser combinators is a powerful approach to parsing which derives much of its power and expressiveness from the type system and semantics of the host programming language. The basics of combinator parsing will be introduced building a small library of combinators, and then using them in an example which will allow us to see how they all fit together.


Speaker: Andrés Sicard-Ramírez and Juan Pedro Villa-Isaza

Talk title: Non-dependent types for the implementation of a dependently typed functional programming language

Abstract: Starting on a Haskell's representation of the terms and types for a theoretical dependently typed lambda-calculus, we will show the Haskell algebraic data types employed for the representation of the dependent types of Agda, a real dependently typed functional programming language.

References: Agda wiki and Simpler, Easier!.


Speaker: Juan Francisco Cardona-Mc'Cormick

Talk title: Introduction to arrows

Abstract: Haskell is plenty of combinators to implement different kinds of computations. "Arrows" are another set of combinators that describes a sort of computation. Arrows are a generalization of monads that enables the composition of complex functions more easier that the monads does. We show the basic features of Arrows and how to compose complex process with them.

Slides: [ pdf ]


Speakers: Francisco José Correa-Zabala and Andrés Sicard-Ramírez

Talk title: Report of IDEAS'09 and 4CCC


Speaker: Juan Francisco Cardona-McCormick

Talk title: Introduction to Pi Calculus


Speaker: Francisco José Correa-Zabala

Talk title: Brief Introduction to Formal Methods


Speaker: Andrés Sicard-Ramírez

Talk title: Induction and Recursion: Two Sides of One Coin

Abstract: Agda is a dependently typed functional programming language and it is a proof assistant, developed at Chalmers University of Technology. Based on the Curry-Howard correspondence, which establish the identification of formulas as types, and proofs as programs; we employ Agda for show the strong relationship between inductive proofs and recursive definitions.


Speaker: Juan Francisco Cardona-McCormick

Talk title: Gramáticas de Atributos

Abstract: Las gramáticas de atributos son un formalismo que permite recorrer árboles definiendo para cada nodo diferentes atributos que pueden depender tanto del contenido del nodo y de sus atributos, como también del contenido de otros nodos adyacentes y los atributos definidos en ellos. Se presentan las gramáticas de atributos, su relación con la programación funcional y su empleo en la definición de la semántica de una gramática abstracta.

Slides: [ pdf ]


Dat​e Talk


Speaker: Juan Pedro Villa-Isaza

Talk title: Regular Expressions Using Haskell

Abstract: Regular expressions are a way to describe text through pattern matching. You might want to use regular expressions to validate data, to pull pieces of text out of larger blocks, or to substitute new text for old text. Today, regular expressions are included in most programming languages as well as many scripting languages, editors, applications, databases, and command-line tools. In Regular Expressions Using Haskell, we show how to use regular expressions with the Haskell programming language, and we give an introduction to the standard library that implements regexps in Haskell, the Text.Regex.Posix library.

Slides: [ pdf ]


Speaker: Sergio Monsalve

Talk title: ACM-ICPC (International Collegiate Programming Contest) problems, approximations and solutions

Abstract: The ACM-ICPC (International Collegiate Programming Contest) is a big oportunity that College students have to demostrate their programming, problem-solving and team working skills. The solutions can be implemented in C, C , Pascal or Java; and these are tested by a robot Judge that operates with basic IO. For some problems of the ICPC we will be presenting some posible solutions in C and Java.


Speaker: Federico Builes

Talk title: Web Programming with Haskell

Abstract: We present an overview of the current state of the art in the web applications field, using Haskell as an implementation language. There have been many different approaches to this problem, from shared memory cloud-like systems to the usual database-backed applications, all of them built on top of the properties of a strictly functional language as Haskell. We review the most updated developments, their problems and how the future looks in this particular area.

Slides: [ url ]


Speaker: Luz Alejandra Parra

Talk title: DNA Computing

Abstract: The aim of the exposition is to make an introduction of matters related with the DNA, begin from the basics of biochemistry language and computation theory. DNA computing is a discipline that aims at harnessing individual molecules at the nanoscopic level for computational purposes. I also will speak about the operation on DNA molecules, and the exposition of the famous Adleman's experiment.


Speaker: Diego Echeverry-Saldarriaga

Talk title: Multi-Objective Optimization for designing Multicast Overlay Networks

Abstract: Overlay Networks have proven to be a possible solution to content distribution, content sharing and Multicast communications. In the case of Multicast Overlay Networks, a balance is needed between the intrinsically conflictive variables (such as Delay and bandwidth) that define the Quality of Service (QoS) of specific applications. One way to achieve this is by optimizing the way the Overlay network is calculated. Our work is the evaluation of different multi-objective evolutionary algorithms (NSGAII, SPEA2) for constructing Overlay networks against naive approaches such as Brute Force or Random Search.


Speaker: Gloria M. Rúa

Talk title: Doxastic Logics SCR-nT4, SCR-nT5, and SCR-nD45

Abstract: We present as extensions of the classical propositional calculus, the hierarchy of deductive systems SCR-n,(with n greater 1). SCR-n is the system of beliefs for agents of type n. The systems are characterized with Kripke-style semantics, in which, the length of the possible world chains is restricted on the type of agent. Moreover, the depth of a model corresponds to the maxim length of the possible world chains that they appear in the model, being that the models of depth n characterize deductive system SCR-(n 1). The SCR-n systems extend, using the theory of the correspondence, to the hierarchies of systems of doxastic logic SCR-nT4, SCR-nT5, and SCR-nD45. Notion of belief is formal in sense of justified knowledge, and conviction, respectively, giving like result systems of doxastic and epistemic logics. They have problem of logical omniscient partially controlled.


Speaker: Manuel Sierra

Talk title: Ilustración de los operadores de afirmación y negación alternas

Abstract: En el sistema deductivo LB, los operadores de afirmación y negación alterna generalizan los operadores de afirmación y negación de la lógica clásica. En esta presentación, siguiendo la definición de verdad presentada por Aristóteles, se ilustra el funcionamiento de estos operadores, al realizar el análisis de la paradoja conocida con el nombre de los cofres de porcia: …… La prueba que inventó parecía de lo más simple: tenía sólo dos cofres, uno de plata y otro de oro, y en uno de ellos se ocultaba su retrato. Las tapas de los cofres tenían las siguientes inscripciones. Cofre de oro: el retrato no está aquí. Cofre de plata: uno y nada más que uno de estos enunciados es verdad. ¿En qué cofre cofre se encuentra el retrato? Pues bien, el pretendiente razonó así: sí la inscripción del cofre de plata es verdad, se da el caso de que uno y sólo uno de los dos enunciados es verdadero, lo que quiere decir que el enunciado del cofre de oro debe de ser falso. Por otro lado, supongamos que el enunciado del cofre de plata es falso, entonces no se dará el caso de que uno y sólo uno de los dos enunciados sea verdad sino que ambos enunciados podrían ser o ambos verdaderos o ambos falsos, pero los dos no pueden ser verdad (ya que asumimos que el segundo es falso), de aquí que ambos sean falsos. Así pues, de nuevo tenemos que el enunciado del cofre de oro es falso, lo que quiere decir que lo mismo que sea verdadero que falso el enunciado del cofre de plata, el del cofre de oro tiene que ser falso, de manera que el retrato tiene que estar en el cofre de oro. Tras razonar así, el pretendiente exclamó triunfante: «El retrato tiene que estar en el cofre de oro», y lo abrió para comprobar horrorizado que estaba vacío. Sin poder comprenderlo insistía en que Porcia le había engañado. Pero Porcia abrió el cofre de plata, el retrato estaba dentro. Bien, ¿dónde se había equivocado el pretendiente en su razonamiento?


Speaker: Raquel Anaya

Talk title: Consideraciones para integrar los métodos formales como práctica en el desarrollo de software

Abstract: Se hara una presentación general del estado actual del desarrollo de software con respecto al uso de lenguajes y formalismos y se plantearan algunas alternativas de acercamiento de los métodos formales de tal manera que fortalezcan la practica del desarrollo de software no solo a nivel academico sino, principalmente, a nivel empresarial. Se contara con la presencia de desarrolladores de la industria quienes tambien nos daran su percepcion acerca del tema.

Slides: [ pdf ]


Speaker: Francisco José Correa-Zabala

Talk title: Integrated framework for the debugging and correction of functional logic programs

Abstract: We present a generic scheme for the declarative debugging of functional logic programs. Our aim is to provide an integrated development environment in which it is possible to debug a program and then correct it automatically. Our methodology is based on the combination, in a single framework, of a semantics-based diagnoser which identifies those parts of the code which contain errors, together with an inductive learner which, once the bug has been located in the program, tries to repair it.


Speaker: Andrés Sicard-Ramírez

Talk title: Programming languages meets program verification: The Chalmers University's approach

Abstract: We will give an overview of the CoVer project (Combining VerificationMethods in Software Development) at Chalmers University, Sweden. The goal of this project is to provide an environment for Haskell programming which provides access to tools for automatic and interactive correctness proofs as well as to tools for testing.Moreover, we will show a short demo of two tools developed aroundCoVer project: Agda, a proof assistant using dependent type theory,and QuickCheck, a property based random testing tool for Haskell.

Slides: [ pdf​ ]