Agda

Se ha publicado un artículo de razonamiento formalizado en Agda sobre metalógica titulado Formalisation in constructive type theory of Stoughton’s substitution for the lambda calculus.

Sus autores son Álvaro Tasistro, Ernesto Copello y Nora Szasz (del Grupo de Computación Teórica (Compute) en la Universidad ORT, Uruguay).

Su resumen es

In Substitution revisited, Alley Stoughton proposed a notion of (simultaneous) substitution for the Lambda calculus as formulated in its original syntax – i.e. with only one sort of symbols (names) for variables – and without identifying α-convertible terms. According to such formulation, the action of substitution on terms is defined by simple structural recursion and an interesting theory arises concerning the connection to α-conversion.

In this paper we present a formalisation of Stoughton’s work in Constructive Type Theory using the language Agda, which reaches up to the Substitution Lemma for α-conversion. The development has been quite inexpensive e.g. in labour cost, and we are able to formulate some improvements over the original presentation. For instance, our definition of α-conversion is just syntax directed and we prove it to be an equivalence relation in an easy way, whereas in Substitution revisited the latter was included as part of the definition and then proven to be equivalent to an only nearly structural definition as corollary of a lengthier development. As a result of this work we are inclined to assert that Stoughton’s is the right way to formulate the Lambda calculus in its original, conventional syntax and that it is a formulation amenable to fully formal treatment.

El trabajo se ha publicado en Electronic Notes in Theoretical Computer Science.

El código de las correspondientes teorías en Agda literario se encuentra aquí.

Se ha publicado un artículo de razonamiento formalizado en Agda titulado Case of (quite) painless dependently typed programming: Fully certified merge sort in Agda.

Sus autores son Ernesto Copello, Álvaro Tasistro y Bruno Bianchi (del Grupo de Computación Teórica (Compute) en la Universidad ORT, Uruguay).

Su resumen es

We present a full certification of merge sort in the language Agda. It features: termination warrant without explicit proof, no proof cost to ensure that the output is sorted, and a succinct proof that the output is a permutation of the input.

El trabajo se ha presentado en The Brazilian Symposium on Programming Languages (SBLP).

El código de las correspondientes teorías en Agda se encuentra aquí.

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.

Se ha publicado un artículo de razonamiento formalizado en Agda titulado Formalising type-logical grammars in Agda.

Su autor es Pepijn Kokke (de la Univ. de Utrecht, Países Bajos).

Su resumen es

In recent years, the interest in using proof assistants to formalise and reason about mathematics and programming languages has grown. Type-logical grammars, being closely related to type theories and systems used in functional programming, are a perfect candidate to next apply this curiosity to. The advantages of using proof assistants is that they allow one to write formally verified proofs about one’s type-logical systems, and that any theory, once implemented, can immediately be computed with. The downside is that in many cases the formal proofs are written as an afterthought, are incomplete, or use obtuse syntax. This makes it that the verified proofs are often much more difficult to read than the pen-and-paper proofs, and almost never directly published. In this paper, we will try to remedy that by example.

Concretely, we use Agda to model the Lambek-Grishin calculus, a grammar logic with a rich vocabulary of type-forming operations. We then present a verified procedure for cut elimination in this system. Then we briefly outline a continuation-passing style translation from proofs in the Lambek-Grishin calculus to programs in Agda. And finally, we will put our system to use in the analysis of a simple example sentence.

El trabajo se ha presentado en TYpe Theory and LExical Semantics.

El código de las correspondientes teorías en Agda se encuentra aquí.