Joint seminar Universidad de Antioquia/Universidad EAFIT
Affiliation: Professor, Departament of Mathematics, Universidad 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.
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
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.
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-105Time: 2:00 p.m. - 3:00 p.m.
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 OrienteTime: 3:00 p.m. - 4:00 p.m.
Title: Girard's Paradox
Time: 2:00 p.m. - 3:00 p.m.
Affiliation: Professor, Departament of Mathematical Sciences, Universidad EAFIT
Title: Introduction to Agda
Slides: N/APlace: Universidad EAFIT, 23-204Time: 2:00 p.m. - 4:00 p.m.
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  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 . 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.
 Conal Elliott. 2017. Compiling to categories. Proc. ACM Programing Languages 1, ICFP, Article 48 (Sept. 2017), 24 pages. https://doi.org/10.1145/3110271
 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.
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.
pdf ]Place: 38-405Time: 11:00 a.m. - 12:00 m.
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.
pdf ]Agda code: GitHub repositoryPlace: 38-501BTime: 5:00 p.m. - 6:00 p.m.
Speakers: Jorge Acevedo-Acosta and José Echeverri-JuradoAffiliation: 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 repositoryPlace: 38-306Time: 5:00 p.m. - 6:00 p.m.
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.
pdf ]Place: 38-501BTime: 5:00 p.m. - 6:00 p.m.
Speaker: Jonathan Prieto-CubidesAffiliation: 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-306Time: 2:00 p.m. - 3:00 p.m.
Speaker: Andreas AbelAffiliation: 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 consideration 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.
pdf ]Video: [ link ]Place: 27-302Time: 2:00 p.m. - 3:00 p.m
Speaker: Alejandro Gomez-LondoñoAffiliation: Proof Engineer at Data61/CSIRO, Australia
Talk title: seL4: Formal verification of an OS kernel  (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" . 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.
 seL4: Formal verification of an OS kernel. Gerwin Klein et al, ACM Symposium on Operating Systems Principles 2009.  seL4 project website
Slides: [ pdf ]Video: [ link ]
Speaker: Elisabet Lobo-VesgaAffiliation: Mathematical Engineer, Universidad EAFIT
Talk title: (Perhaps Less Simple) Monadic Equational Reasoning
Speaker: Jonathan Prieto-CubidesAffiliation: 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ónAffiliation: 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.
Speaker: Alejandro Calle-SaldarriagaAffiliation: 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.
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 ]
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.
Speaker: Alejandro Gómez Londoño
Talk title: Overview of ICFP 2015
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.
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.
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 ]
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.
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.
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.
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 ]Code
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.
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
Speaker: Néstor Cataño-Collazos
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.
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.
Talk title: Enoch: Not the father of Methuselah
Abstract: We explore mathematical monads and their relation to monads in Haskell and Agda.
Talk title: Enoch: The father of Irad
Abstract: We explore natural transformations and their relation to polymorphic functions in Haskell and Agda.
Talk title: An Introduction to Erlang
Abstract: An overview of the history and some basic functional and concurrent concepts of Erlang.
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.
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.
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.
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 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" and functional reactive programming (FRP) as a possible solution to these issues.
 Gerald Jay Sussman and Guy L. Steele, Jr. "Scheme: An interpreter for extended lambda calculus". AI Memo 349: 19, December 1975.  Edsger W. Dijkstra. Go To Statement Considered Harmful. Communications of the ACM, Vol. 11, No. 3, March 1968, pp. 147-148.
Speaker: Andrés Eugenio Castaño-Cardenas
Talk title: Abstract Interpretation
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.
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.
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.
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.
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.
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 ]
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.
Talk title: Proofs = Programs
Abstract: From the Agda Wiki:
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.
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.
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.
Speakers: Francisco José Correa-Zabala and Andrés Sicard-Ramírez
Talk title: Report of IDEAS'09 and 4CCC
Talk title: Introduction to Pi Calculus
Speaker: Francisco José Correa-Zabala
Talk title: Brief Introduction to Formal Methods
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.
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.
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.
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.
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.
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.