ProgLog Meetings in 2006

Past meetings of 2006.

Date Speaker Title Extra
Dec 15 Sergei Soloviev Non-standard reductions in typed lambda-calculus with inductive types and normalization properties, at 11.15, in room 5453 abstract
Dec 13 Thomas Hallgren Operating system construction in Haskell and some ideas on using dependent types abstract, ICFP2005 paper
Dec 6 Conor McBride Epigram 2: the core story, video seminar with AIST and Nottingham, at 9.00, in SGSR abstract
Nov 29 Nils Anders Danielsson A Simple Library for Semi-Formal Verification of the Time Complexity of Purely Functional Data Structures abstract
Nov 22 Arnaud Spiwack Towards efficient computation in Coq abstract
Nov 15 Ana Bove Computation by Prophecy abstract
Nov 8 Ulf Norell A type-safe treatment of meta variables abstract
Nov 1 Aarne Ranta Compiling GF abstract
Oct 25 Peter Dybjer The history of the identity type abstract
Oct 18 Bas Spitters Constructive analysis, types and exact real numbers. abstract, [Spitters], [O'Connor]
Oct 11 Thierry Coquand Getting Pi right in Set abstract, slides
Oct 4
meeting
Sep 27
No ordinary ProgLog meeting during AIM5
Sep 20 Thierry Coquand informal reports abstract
Sep 13 Fredrik Lindblad Finding Counterexamples and Proofs using Meta Variables in Functional Programs abstract
Sep 6 David Wahlstedt Dependent Type Theory with Parametric First-Order Data Types and Pattern-Matching abstract
Aug 30 Andres Sicard Hypercomputation abstract
Aug 23 Nils Anders Danielsson A definition of a dependently typed language as an inductive-recursive family abstract
Jun 16 Norio KATO Exploiting Type Information to Compile Agda into Haskell, video seminar with AIST, at 9.00 in video conf. room, AV-centralen, V-house abstract
Jun 14 Michael Hedberg Verifying Warshall's algorithm in Agda, room 6128 abstract
Jun 7 Peter Dybjer Normalization by Evaluation for Martin-Löf Type Theory with One Universe abstract
May 31 Patrik Jansson Testing properties of generic functions abstract
May 10 Ulf Norell Agda II -- Take One, video seminar, at 9.00 in video conf. room, AV-centralen, V-house abstract
May 3
AIST-collaboration
Apr 26 Fredrik Lindblad Proof Search by Lazy Instantiation of First-Order Terms abstract
Apr 12 Bengt Nordström Interaction with a Proof Editor abstract
Apr 5 Andreas Abel Sized (Co-)Inductive Types (With Applications to Generic Programming) abstract
Mar 29 Ana Bove General Recursion and CoInductive Types abstract
Mar 22 Thierry Coquand Typing Rules for Agda 2, video seminar with AIST, at 9.00 in video conf. room, AV-centralen, V-house
Mar 15 Jordi Saludes Generating natural language for mathematical exercises abstract, link
Mar 15 Tamara Rezk Certificate translation, at 10.15 in 5453 abstract
Mar 8 Carlos Gonzalía Relations in Dependent Type Theory abstract
Mar 6 Masahiko Sato Abstraction and Substitution by Frege-Gentzen Approach, NOTE: irregular day and time: Monday, Mar 6, at 15.15, in 5453 abstract
Mar 1
Meeting to discuss: VR-applications, webpages, TYPES workshop
Feb 22 David Wahlstedt Proving Reducibility of Recursively Defined Constants abstract
Feb 16 Danko Ilik Zermelo's well-ordering theorem in type theory, Thursday, 11.00, ES63, Master's thesis pres
Feb 8 Ulf Norell Implicit arguments in Agda2 abstract


Abstracts of talks in 2006


Non-standard reductions in typed lambda-calculus with inductive types and normalization properties, at 11.15, in room 5453
(Joint work with D. Chemouil and F. Barral)

Date: Dec 15
Speaker: Sergei Soloviev (IRIT, Toulouse)
Abstract:
One of well known difficulties encountered in the applications of proof-assistants based on type theory is that many equalities that a user expects for granted are satisfied only extensionally (not supported by reduction mechanisms). We study some reductions that may be added preserving SN and CR property and ?transform? certain useful equalities into intensional w.r.t. the extended system. (For example, invertibility of some functions.) Main results concern simply typed lambda-calculus with inductive types. We consider isomorphisms between copies of inductive types, products, finite types. The problem of functoriality of a schema of an inductive type with parameters is studied. Some possibilities of generalization to the systems with dependent types are considered.
The talk is based on joint work with D. Chemouil (former ph.d. student) and F. Barral (ph.d. in progress).


Operating system construction in Haskell and some ideas on using dependent types

Date: Dec 13
Speaker: Thomas Hallgren
Links: ICFP2005 paper
Abstract:
First, I present "A Principles Approach to Operating System Construction in Haskell" (from ICPF 2005), where we describe a monadic interface (the H monad) to low-level hardware features that is a suitable basis for building operating systems in Haskell. Its behavior is specified in part by formal assertions written in a programming logic called P-Logic.

While most memory safety requirements can be captured in the types of the H monad operations, and checked at compile-time, some checks (bounds checks) have to be deferred until run-time. So, second, I describe a little experiment using dependent types to move more checks to compile-time, further reducing the risk that programmer mistakes go undetected until run-time, and potentially also improving performance.


Epigram 2: the core story, video seminar with AIST and Nottingham, at 9.00, in SGSR

Date: Dec 6
Speaker: Conor McBride
Abstract:
Not much of Epigram 2 actually exists yet, but I can give you some idea of what it will be like, on the outside and on the inside. I'll give an overview of the system's structure, then focus on the key ideas and methods which are central to Epigram 2. The crucial idea, carrying over from Epigram 1, is to separate the source language from the core type theory, thus reducing the tension between the design imperatives of convenience for the former and simplicity for the latter.

I shall concentrate mainly on on our new core. We now distinguish syntactically between the terms whose types may be synthesised and those whose types must be prescribed. This choice has had a significant impact on the way we think about data in Epigram. Rather than equipping our system with the means to add new datatypes to our type theory, we directly add a universe of datatypes whose codes are themselves data.

This has been a team effort, thanks to Thorsten Altenkirch and his PhD students. Specifically, this talk is largely based on a collaboration with James Chapman and Peter Morris.


A Simple Library for Semi-Formal Verification of the Time Complexity of Purely Functional Data Structures

Date: Nov 29
Speaker: Nils Anders Danielsson
Abstract:
Okasaki and others have demonstrated how purely functional data structures that are efficient even in the presence of persistence can be constructed. The associated time complexity analysis often requires careful attention to detail, and hence formalising it is valuable.

This work describes a simple library that can be used to formalise the analysis of a class of purely functional data structures. The basic idea is to use the type system to annotate all functions with the time required to compute their result. An annotated monad is used to combine time complexity annotations. The library has been implemented and used to analyse some existing data structures, for instance (parts of) the finger trees of Hinze and Paterson.

It is also sketched how amortised data structures analysed using the library can be automatically turned into worst-case ones.


Towards efficient computation in Coq

Date: Nov 22
Speaker: Arnaud Spiwack
Abstract:
With growing activity, the users of Type Theory tend to need more and more computation, both to use Type Theory as a reasonable programming language and to make proofs with a big computational content. I shall focus on the proof assistant Coq, and show how to use the existing structures (in particular the Virtual Machine) to add efficient natural numbers computation at a minimal cost. This is done in two mostly independant steps : the choices and constraint of representation inside Coq's virtual machine, and the representation seen by the user. In order to glue both together, we introduce a mechanism called "retroknowledge", whose main goal is to internalize into the theory (Coq's kernel) some meaningful parts of the user's developpement.


Computation by Prophecy
(Joint work with Venanzio Capretta)

Date: Nov 15
Speaker: Ana Bove
Abstract:
On one hand, we have the Bove-Capretta (inductive) method to define partial and general recursive functions in type theory.
On the other hand, we have Venanzio Capretta's paper showing how one could use co-inductive types to represent partiality in type theory. Can we combine both method and define a Bove-Capretta (co-inductive) method which has the advantages of both previous work?

Those of you who were at TYPES meeting in Nottingham might think you have already listen to this talk! But you are only partly right...

In the talk on Wednesday I will present a new method to represent general recursion and partiality in type theory using co-inductive types which is much more efficient than the one presented by Venanzio at the meeting in Nottingham. I will also show how to prove that the recursive equations are still valid.


A type-safe treatment of meta variables

Date: Nov 8
Speaker: Ulf Norell
Abstract:
I will present the work Catarina and I have been doing on meta variables. There will be typing rules, examples, and live demos. See below for a more technical description of the problem we are solving.

In type theory the convertibility rule states that if t : B and A = B then t : A, where A = B means that A and B have the same normal form. To implement this rule a type checker can simply normalise A and B and check if the normal forms are equal. However, in the presence of meta variables this is no longer possible: A and B might contain meta variables preventing them from being normalised. Instead A and B are unified, possibly instantiating some of the meta variables. The unification can have three different outcomes:
  yes - found a unique instantiation which makes A = B
  no - no instantiation makes A = B
  maybe - couldn't find a unique instantiation, but one could still exist
The troublesome case is the third one. In previous implementations of Agda the approach have been to accept t : A but remember the constraint A = B. The problem with this is that if a meta variable is later instantiated making A and B different you have an ill-typed term t on your hands. Our solution is to replace t by a fresh constant c : A = t whose definition is only accessible if A = B.


Compiling GF

Date: Nov 1
Speaker: Aarne Ranta
Abstract:
GF is a grammar formalism, i.e. a special purpose programming language for writing grammars. It is a functional language with dependent types. A GF program (a grammar) is a declarative definition of a language, on a high abstraction level that improves grammar writing productivity.

To compile a GF grammar is to generate lower-level code that performs two computational tasks:
- linearization: take syntax trees to strings
- parsing: take strings to syntax trees

The talk gives an overview of the compilation process, as well as snapshots of some special problems, in particular
- the module system and separate compilation
- back-end optimizations of grammars
- grammar checking as type checking


The history of the identity type

Date: Oct 25
Speaker: Peter Dybjer
Abstract:
I will talk about the history of the identity type. I will start with the letter of Howard to Kreisel in 1969, and will continue with the accounts of identity by Lawvere 1970, Scott 1970, Martin-Löf 1971, 1972, 1973, 1979, and 1986. If time permits I will also say something about the more recent findings about the identity type.


Constructive analysis, types and exact real numbers.
(Joint work with Herman Geuvers, Milad Niqui and Freek Wiedijk)

Date: Oct 18
Speaker: Bas Spitters (Institute for Computing and Information Sciences, Radboud University, Nijmegen)
Links: [Spitters], [O'Connor]
Abstract:
We will discuss various aspects of computable/constructive analysis, namely semantics, proofs and computations. We will present some of the problems and solutions of exact real arithmetic varying from concrete implementations, representation and algorithms to various models for real computation. We then put these models in a uniform framework using realisability, opening the door for the use of type theoretic and coalgebraic constructions both in computing and reasoning about these computations. We will indicate that it is often natural to use constructive logic to reason about these computations.

Finally, I will scrupulously show the work of Russell O'Connor on the "FewDigits"-implementation of exact real numbers in Haskell and Coq.

Literature:
* Constructive analysis, types and exact real numbers. (with Herman Geuvers, Milad Niqui and Freek Wiedijk) to appear in Constructive analysis, types and exact real numbers, special issue of Mathematical Structures in Computer Science (Bas Spitters, Herman Geuvers, Milad Niqui and Freek Wiedijk(eds.)) MSCS 2006.
http://www.cs.ru.nl/~spitters/editorial.pdf
* http://r6.ca/FewDigits/


Getting Pi right in Set

Date: Oct 11
Speaker: Thierry Coquand
Links: slides
Abstract:
After the discussions about "Pi in Set" at the last AIM5 I got new inputs from Peter and Andreas (and Klaus Aehlig). These suggest a systematic method, based on normalisation by evaluation, to prove the desired metaproperties of a type system with universes and strong conversion rules (eta conversion, but also surjective pairing or conversion rules for singleton types). It gives also an elegant way to program the conversion algorithm, which fits well with the current implementation of core agda.
I will present the formal system (type theory with universes with conversion as judgements), its PER semantics and the associated normalisation and conversion algorithms. I will then argue that, provided the proofs of correctness and completness of these algorithms are valid, this formal system should be the basis of Agda 2 (instead of the Logical Framework).

The slides are available.


informal reports

Date: Sep 20
Speaker: Thierry Coquand
Abstract:
This will be very informal. I will report quickly on a few things that I found interesting at some meetings I have just attended. I should present:
-a surprising Haskell program, by Martin Escardo and Ulrich Berger, with which we can write, in a total way, universal and existential quantifications over an infinite data type (good approximation of the halting problem)
-some examples by Helmut Schwichtenberg of program extractions in minlog (at least square root functions [1,4] -> [1,2] extracted from a general lemma about existence of inverse functions)
-the complete mechanization of Hessenberg's Theorem by Marc Bezem and Dimitri Hendriks (stating that Pappus axiom implies Desargues axiom), in type theory connected with a special first-order prover


Finding Counterexamples and Proofs using Meta Variables in Functional Programs

Date: Sep 13
Speaker: Fredrik Lindblad
Abstract:
At my previous ProgLog presentation I described some experiments in adding meta variables to a functional language and doing search. The idea was applied on program verification by finding counterexamples for functional properties, and on finding proofs by implementing a proof checker. The search algorithm is based on two main ingredients; lazy instantiation and parallel evaluation.
I will continue on these two tracks and also discuss the relation to Curry, a functional logic language, in particular the concepts of narrowing and concurrent constraints.


Dependent Type Theory with Parametric First-Order Data Types and Pattern-Matching

Date: Sep 6
Speaker: David Wahlstedt
Abstract:
We present a variation of Martin-Löf's logical framework with $\beta\iota$-equality, extended with first-order parametric data types and constants defined recursively with pattern-matching. We use the \emph{Size-Change Principle for Program Termination} (C.S. Lee, N.D. Jones, A. Ben-Amram 2001) to justify the recursive definitions. This approach enables us to define new constants in a straight-forward manner. Our contribution is a proof of normalization for the proposed system.


Hypercomputation

Date: Aug 30
Speaker: Andres Sicard
Abstract:
While the idea of an absolute computability (i.e. Turing machine computability), detached from logical, mathematical, physical or biological theories is hard to hold nowadays, the idea of a relative computability has progressively gained supporters, as shown by the establishment of an academic community around hypercomputation theory (i.e. computing beyond Turing machine's limit). In this talk we will show some hypercomputation models, the relation between hypercomputation and the Church-Turing thesis, and our results on the possibility of hypercomputation based on quantum computation.


A definition of a dependently typed language as an inductive-recursive family

Date: Aug 23
Speaker: Nils Anders Danielsson
Abstract:
I have defined an inductive-recursive family (in Haskell terms: a fancy GADT) for a simple dependently typed language in agdaLight. I will discuss the definition, including some design choices and termination issues. If there is time I will also illustrate that it is seemingly convenient to write programs using this definition by showing a normalisation result (the proof uses normalisation by evaluation).


Exploiting Type Information to Compile Agda into Haskell, video seminar with AIST, at 9.00 in video conf. room, AV-centralen, V-house

Date: Jun 16
Speaker: Norio KATO
Abstract:
I will present an optimizing translator from Agda to Haskell. The translator attempts to compile Agda datatypes into their natural counterparts in Haskell so that runtime overheads will be reduced. General untyped representation is used for those types for which no such counterparts have been found. Some empirical results and present problems will be shown.


Verifying Warshall's algorithm in Agda, room 6128

Date: Jun 14
Speaker: Michael Hedberg
Abstract:
The algorithm is about finding the transitive closure of a boolean square matrix.
Rather than formalizing a mathematical model of the imperative language in which the algorithm is naturally expressed, the algorithm is "manually" transformed into a functional program.
The functional program may with some effort be shown to be equivalent to another program which is more easily seen to be correct.
The difference between the two programs lies in treatment of vector assignment.
The safe way to do X:= f(X) for vector X is to use temporary vector T: FOR i:= ... DO T[i]:= f(X)[i];FOR i:= ... DO X[i]:=T[i].
The abovementioned "effort" lies in justifying the unsafe implementation: FOR i:= ... DO X[i] := f(X)[i].


Normalization by Evaluation for Martin-Löf Type Theory with One Universe

Date: Jun 7
Speaker: Peter Dybjer
Abstract:
It is a somewhat updated version of the talk I gave in Japan last month on joint work with Andreas Abel and Klaus Aehlig.
I will start with an introduction to normalization by evaluation and intuitionistic model construction. Then I will explain how to write an algorithm for normalization in Gödel System T, and how to prove it correct. Finally, I will show how this algorithm needs to be modified in order to yield an algorithm for Martin-Löf type theory with one universe.


Testing properties of generic functions

Date: May 31
Speaker: Patrik Jansson
Abstract:
Generic functional programming is a paradigm for expressing generic algorithms parametrized by types. Examples of such algorithms are equality tests, traversals and pretty printers. Concrete instances can be obtained by instantiating a template algorithm with (the structure of) a datatype.
Generic functions satisfy generic properties. Since generic functions essentially consist of several functions combined in one, testing or proving properties of generic functions becomes harder.
In this talk I will show how properties of generic functions in Generic Haskell can be formulated and tested using QuickCheck. (And more interestingly, what cannot easily be formulated or tested.)


Agda II -- Take One, video seminar, at 9.00 in video conf. room, AV-centralen, V-house

Date: May 10
Speaker: Ulf Norell
Abstract:
I will present the first version of the Agda II language and some of the motivations behind it. In particular I will talk about what is in the language: and what is not: and try to convey the reasons why this is so. The presentation will be accompanied by a healthy amount of simple examples illustratating the syntax of the language and how the different features can be used.


Proof Search by Lazy Instantiation of First-Order Terms

Date: Apr 26
Speaker: Fredrik Lindblad
Abstract:
The method that underlies the systematic construction of terms in Agsy (the proof search tool for Agda) can be described as "lazy instantiation", i.e. instantiate what you need in order to proceed with the lazy evaluation. I will examplify this by applications in automatic testing and function synthesis.
The same idea can be applied on the construction of first-order terms, leading to a very simple, Prolog-like system. I will demonstrate a compiler for a small functional language, which supports search by lazy instantiation.
A natural question is whether proof search (in Agda) is itself appropriate to formulate as a problem in such a language. This would amount to writing a typechecker and then running a search where the type but not the term is specified. I will present some ideas on the viability of representing Agsy in this way.


Interaction with a Proof Editor

Date: Apr 12
Speaker: Bengt Nordström
Abstract:
The idea is that the user of an editor for proofs (or programs, or documents) should be able to use text-editing and structure-editing freely. The editors alfa and half developed earlier in the department have mainly been structural editors where all parts of the proof/ program always have been type-correct. We want to loosen the straight- jacket of always being correct. (At least when it comes to proving.)


Sized (Co-)Inductive Types (With Applications to Generic Programming)

Date: Apr 5
Speaker: Andreas Abel (Ludwig-Maximilians Universität, Munich)
Abstract:
A type system for recursive and corecursive functions over equi-inductive and -coinductive types is presented in which all programs are strongly normalizing. The type system supports data types of higher kind and arbitrary rank polymorphism and therefore accepts recursive functions whose termination cannot be shown with methods based on term orderings alone. (Such functions typically arise in generic programming.)

The choice of equi-inductive types, instead of the more common iso-inductive types, influences both reduction rules and the strong normalization proof. By embedding iso- into equi-types, the latter ones are recognized as more fundamental. A model based on orthogonality is constructed where a semantical type corresponds to a set of observations, and soundness of the type system is proven.


General Recursion and CoInductive Types

Date: Mar 29
Speaker: Ana Bove
Abstract:
On one hand, we have the Bove-Capretta (inductive) method to define partial and general recursive functions in type theory.
On the other hand, we have Venanzio Capretta's paper showing how one could use coinductive types to represent partiality in type theory.
Can we combine both method and define a Bove-Capretta (co-inductive) method which has the advantages of both previous work?

In this talk I will assume you know about the BC (inductive method) (otherwise you can get a copy of my PhD thesis, a bit more than 200 pages! :-) and I will present some of the ideas in Venanzio's paper "General Recursion via Coinductive Types". While presenting Venanzio's work, I intend to show how to prove properties coinductively. Besides a white-board explanation, I will demonstrate the Coq proof assistant for these kind of proofs. So this talk can be thought of as a very informal and very basic tutorial on coinductive types and proofs. Be aware I have only worked with coinductive types for a short while, so I won't have many of the answers you might be looking for!

The talk will end with some words on how to combine both methods. Hopefully, this will be the topic of one of the talks at TYPES.


Generating natural language for mathematical exercises

Date: Mar 15
Speaker: Jordi Saludes (Universitat Politècnica de Catalunya (Barcelona))
Links: link
Abstract:
The main goal of the webALT project is providing a repository of calculus and linear algebra exercises for freshmen that can be automatically rendered in different languages from encoded semantics. The Grammar Framework is the tool driving the exercise editor and providing these renderings.


Certificate translation, at 10.15 in 5453
(Joint work with G. Barthe, B. Gregoire, and C. Kunz)

Date: Mar 15
Speaker: Tamara Rezk (INRIA Sophia-Antipolis)
Abstract:
Program verification techniques based on programming logics and verification condition generators provide a powerful means to reason about programs. Whereas these techniques have very often been employed in the context of high-level languages in order to benefit from their structural nature, it is often required, especially in the context of mobile code, to prove the correctness of compiled programs. Thus it is highly desirable to have a means of bringing the benefits of source code verification to code consumers.
We propose certificate translation, a mechanism that allows to transfer evidence from source programs to compiled programs. It builds upon the notion of certificate, which is used in Proof Carrying Code architectures to convey to the code consumer easily verifiable evidence that programs respect some policy. A certificate translator is an algorithm that turns certificates of source programs into certificates of compiled programs; its definition is tightly bound to the compiler used for programs, and the main difficulty in defining one stems from the optimizations performed by the compiler. In order to illustrate the feasibility of our approach, we build certificate translators for an optimizing compiler from a simple imperative language to an intermediate RTL language.


Relations in Dependent Type Theory

Date: Mar 8
Speaker: Carlos Gonzalía (Chalmers)
Abstract:
This thesis investigates how to express and reason about relational concepts and methods inside the constructive logical framework of Martin-Löf's monomorphic type theory. We cover several areas where the notion of relation is central, and show how to formalize the basic concepts of each area. This formalization is carried out in a computer proof assistant for Martin-Löf's type theory called Agda/Alfa, and this software allows the practical handling of the numerous technical details involved in such a task.

The first area we investigate is relations and relational systems themselves. Many of the relational systems in use within computer science are based on algebras that extend Boolean algebra, and hence are unsuitable for a constructive framework. Instead we use the constructive algebra of relations provided by the categorical theory of allegories. First, we introduce the notion of an E-allegory, the appropriate abstract notion of an allegory formalizable in Martin-Löf type theory. Then we set up two concrete instances: the E-allegory of E-relations, and the E-allegory of finite decidable E-relations. We investigate further properties of the E-allegories and note that only the latter satisfies the axioms of a power allegory and a Boolean allegory.

The second area is relational program construction and derivation. Martin-Löf type theory provides its own approach to program construction via the identification of propositions and types, and our goal is to supplement this methodology with techniques from relational programming. Here we note that Martin-Löf type theory is based on a functional notion of program, and provides a logical setting where we can reason about the connections between functional and relational notions of programs. We show some links and differences with type-theoretic program construction and derivation. We then show how recursive relations can be dealt with in type theory using the concept of relational catamorphism.

The third area is the relational database model. This data model has similarities and connections with relational algebras and allegories, but presents new problems in the way typings are handled via schemes and attributes. We set up an increasingly complex series of formalizations of the relational model, with different decidability characteristics and with respect to the way in which the scheme/attribute typing issues are handled. The final formalization, which is both the most complex and the most satisfactory, is built on an abstract finite set layer, and can be seen as an abstraction for implementations of database managers.


Abstraction and Substitution by Frege-Gentzen Approach, NOTE: irregular day and time: Monday, Mar 6, at 15.15, in 5453

Date: Mar 6
Speaker: Masahiko Sato (Kyoto University)
Abstract:
Frege and Gentzen used two disjoint sets of variables, namely the sets of free variables and bound variables, as the basic building blocks for constructing syntactic entities like propositions and proofs. For Frege, in particular, free variables are always tied with the notion of inference which enables us to proceed from already asserted judgments to a new judgment.
In this talk, we will follow Frege-Gentzen approach, and will show that substitution can be defined without appealing to the notion of alpha-equivalence, and also show that we can define alpha-equivalence more naturally compared to traditional approach. It is hoped that this approach is useful in practice for implementing proof assistant systems on a computer.


Proving Reducibility of Recursively Defined Constants

Date: Feb 22
Speaker: David Wahlstedt
Abstract:
I will, informally and in interaction with you, present a problem I'm currently facing.
Im working on an extension of the result presented in my Licentiate dissertation, which was to prove normalisation for a combination of a framework similar to Martin-Löf's LF and dependently typed recursive pattern-matching definitions, justified by the "size-change principle for program termination" (Lee, Jones, Ben-Amram '01). However, the system was restricted to non-parametric data types and computation rules not taking functions as arguments, nor returning functions. The introduction of parametric data types seems to be an easy extension so far, and the important parts of the old normalisation proof are essentially unchanged. The idea is now to relax the restriction on recursive computation rules, and allow functions both in the arguments and in the result. We should also allow curried functions.
When looking at the old proof, there is no good reason it shouldn't scale up, but of course I need a better argument ;->
I have an over all structure of a proof that seems convincing, but it is difficult to get the details right, and this is crucial.
I will first try to "throw you into the core problem" in an informal way, and then (after a break ?) try to explain some technical aspects. I will not talk about size-change termination here, since this is just a special (though quite general) case of an abstract property assumed in this part of the proof.


Implicit arguments in Agda2

Date: Feb 8
Speaker: Ulf Norell
Abstract:
I will talk about implicit arguments in Agda2. More specifically a strategy for figuring out were the implicit arguments should go.
Notation:
{x:A} -> B is the hidden pi
f {x} is the explicit application of an implicit argument
? is a meta variable
\{x:A} -> t is a hidden lambda (of type {x:A} -> B)
\{x} -> t is a domain-free hidden lambda

We want to define a transformation that inserts meta variables for implicit arguments in a term. Below I will call this transformation -->

Examples:

Assume id : {A:Set} -> A -> A
then id x --> id {?} x

What about 'id'?
id --> id {?}
or id --> id

How about higher order hiding?

foo : ({A:Set} -> A -> A) -> N -> N
foo g n = g n

foo id 0 --> foo id 0 -- ?

bar : {A:Set} -> (A -> A) -> A -> A
bar g n = g n

bar id 0 --> bar {N} (id {N}) 0

In the meeting I will present a powerful yet elegant algorithm for this transformation.