Logic and Computation Seminar

Abstract:
The lambda calculus is a well-studied model of computation with deep significance in type theory, whose foundational results often exhibit considerable technical complexity. In this seminar, we present a formalization of the lambda calculus in the Lean proof assistant, based on the De Bruijn index representation. This approach streamlines the definition of terms and syntactic operations, thereby simplifying both the construction and maintenance of proofs.
Slides (Spanish)

Abstract:
This presentation introduces the formalization of some basic concepts in category theory using the dependently typed programming language and proof assistant Agda. It begins with intuitive explanations of categories, morphisms, and commutative diagrams, presenting classical mathematical examples such as the category $Set$, $\mathbb{N}$ with $\le$, and monoids as single-object categories. It then develops the formalization of these structures in Agda, covering inductive definitions, identity and associativity proofs, as well as the implementation of the categorical laws. The work culminates in the formalization of functors as structure-preserving morphisms between categories. This project demonstrates Agda’s expressive power for encoding mathematical abstractions and outlines future directions for formalization. Code examples and a GitHub repository are included to facilitate reproducibility and further exploration.
Slides

Abstract:
The Kirby–Paris Hydra Game presents a fascinating paradox: despite appearing to expand exponentially during play, the game invariably terminates after a finite number of steps. This property relates to fundamental limits in formal systems, particularly Peano arithmetic. In this paper, we present a simplified formalization of the Hydra Game using the Coq proof assistant. We represent hydras as rose trees and develop a lexicographic termination proof based on counting nodes at each level. This representation allows us to establish that each game step produces a lexicographically smaller list, guaranteeing termination. We present the key theorems and lemmas of our formalization, explaining their intuitive meaning and formal significance within the proof structure. Our work demonstrates the application of interactive theorem proving to verify properties of combinatorial games with deep connections to mathematical logic, and provides an accessible case study of formal verification using the Coq proof assistant.
Slides1, Slides2

Abstract:
In 1995, Barendregt proposed a conjecture at Typed Lambda Calculi and Applications regarding Pure Type Systems (PTS): if a PTS is weakly normalizing, then it is also strongly normalizing. To date, this conjecture remains open, though some partial results have been achieved.

First, Barthe, Hatcliff, and Sørensen (2001) proved the conjecture for a subclass of PTSs—the Generalized Non-dependent PTSs, in which types do not depend on terms. Second, Harper and Lillibridge (1993) showed that certain extensions of PTSs, involving additional sorts and rules that preserve normalization, can be used to provide further evidence for the conjecture. Finally, more recently, Mull (2022) introduced a new class of PTSs—Tiered PTSs—through which questions about normalization can be addressed more effectively.

To extend these results, two promising approaches can be pursued, both based on the concept of lambda-I terms. The first approach is to extend the work of Barthe, Hatcliff, and Sørensen (2001) by defining translations from general expressions to lambda-I expressions. The second is to generalize the definition of lambda-I expressions and extend the Conservation Theorem of the untyped lambda calculus.
Slides

Abstract:
Esta charla tiene como objetivo presentar el uso de algunos modelos de inteligencia artificial como lo son los modelos extensos del lenguaje (Llms) en el proceso de formalización de demostraciones matemáticas en el asistente Lean. Específicamente, vamos a exponer el framework LeanCopilot que permite automatizar la formalización a través de la sugerencia de tácticas o la búsqueda de nuevas demostraciones en Lean. Además de esto, vamos a presentar un caso de la comunidad matemática que hace explicita la necesidad de usar formalizadores computacionales para verificar formalmente un teorema.
Slides

Abstract:
La matemática como disciplina científica tiene un estatus especial porque, se supone, sus métodos son rigurosos. Si bien no lo hacemos todos los días (ni mucho menos) asumimos que, si nos fuerzan a ello, podríamos transformar nuestras pruebas (que surgieron de nuestra intuición) en deducciones formales dentro de un sistema lógico con axiomas aceptados por la comunidad del área en cuestión. Bourbaki dedicó todo un capítulo para sentar su sistema formal pero en el prefacio se aclara que tampoco es tan necesario por eso mismo que decíamos: es algo tedioso, poco informativo y muy demandante.

Siendo que la matemática trata con estructuras cada vez más complejas es posible que debamos aceptar que la traducción es cada vez más difícil pero cada vez más necesaria. Para facilitarnos la vida podemos aprovechar la tecnología de los asistentes de prueba (de la misma manera que usamos Maple, Mathematica, o Geogebra para calcular cosas) y escribir nuestras pruebas en programas que no sólo verifican la validez de nuestras deducciones sino también nos asisten en la construcción de las derivaciones.

En esta charla repasaré algunas de las cuestiones mencionadas más arriba citando a gente que sabe más que yo y mostraré ejemplos de formalizaciones en dos asistentes de prueba distintos.
Slides (Spanish)

Abstract:
El estudio de las estructuras y el orden es esencial en numerosos campos, como las matemáticas y la computación. Este análisis proporciona un marco para comprender sistemas complejos, facilita la resolución de problemas y fomenta el pensamiento lógico. En particular, la teoría de categorías y las estructuras de restricción constituyen herramientas poderosas para modelar y analizar relaciones complejas.

En la charla, exploraré algunos conceptos fundamentales de la teoría de categorías, tales como categorías, functores y transformaciones naturales. Estos elementos ofrecen una perspectiva única sobre las estructuras matemáticas y sus interrelaciones. Además, abordaré importantes construcciones y el concepto de estructuras de restricción.
Slides (Spanish)

Abstract:
En tu día a día, es probable que uses Discord para charlar y compartir con comunidades y amigos, o WhatsApp para ver las imágenes de Piolín que te envían tus tías. Pues detrás de estos gigantes tecnológicos, está siendo impulsada una misteriosa máquina: BEAM. Esta será una introducción a la historia, el ecosistema y los casos de uso de este fenomenal entorno.
Talk repository

Abstract: N/A

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

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

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 (Spanish)

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

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 (Spanish)

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

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.

Abstract: N/A
Slides

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

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

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 proof assistants, and in foundational studies of Type Theory.
Slides

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

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 and Agda code

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

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

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

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

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

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

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

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.

References:

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

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

Abstract: N/A
Slides

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

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.

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).

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

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.

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

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

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

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

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

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

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

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

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

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

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

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

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.

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

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

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.

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

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

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.
Slides1, Slides2

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.

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

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.

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

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

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 (Spanish)

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.

Abstract: N/A

Abstract: N/A

Abstract: N/A

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

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!.

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.

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

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

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.

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

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

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.

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?

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.

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.

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.

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

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.

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