ProgLog Meetings in 2008
Past meetings of 2008.
Abstracts of talks in 2008
Program Testing and Constructive Validity
Date: Dec 10
Speaker: Peter Dybjer
Abstract:
In this talk I discuss the connection between Martin-Löf's meaning explanations and program testing. First I give an overview of the historical development of the ideas behind the meaning explanations. Then I explain the connection with program testing. Finally, I discuss the relevance of the testing point of view on some other logical systems and constructive principles.
A type-theoretic view of dynamic logic and DRT
Date: Nov 12
Speaker: Philippe de Groote (Inria-Lorraine, France)
Abstract:
We propose a formalization of DRT within Church's simple theory of type. This formalization, which allows DRT and Montague semantics to coexist within the same framework, is such that the notions of free and bound occurrences of a variable are the usual ones. We then extract from it the underlying dynamic logic.
(DRT = Discourse Representation Theory)
A Calculus of Definitions, revisited
Date: Nov 5
Speaker: Thierry Coquand
Links: slides
Abstract:
I will first present what should be a simplification of Mini-TT, a simple type-theoretic language. I will describe an operational semantics and a denotational semantics for this language, such that a term is SN whenever its denotation is not bottom.
This core language does not have inductive families but it will be shown that several examples which seem to require inductive families can be presented, such as the type BSTree used in the course of Ana and Peter. Another nice example is Peano induction for binary numbers, discussed by Conor in the FP Lunch weblog.
Correctness by design -- an exercise in dependently typed programming
Date: Oct 15
Speaker: Ulf Norell
Abstract:
This is a joint proglog meeting and lecture in the course Types for programs and proofs.
Synthesis of Equational Logics from Algebraic Meta-Theories
Date: Sep 24
Speaker: Marcelo Fiore (Computer Laboratory, University of Cambridge)
Abstract:
I will present a mathematical methodology for the synthesis of (in)equational deductive systems, that are sound and complete for a canonical algebraic model theory; see [1].
As a running example, I will show how the methodology applies to rationally reconstruct the traditional equational logic of universal algebra from general principles.
As for modern applications, I will indicate how to use the methodology to synthesise: (i) a nominal equational logic (for specifying algebras with variable binding), see [1, Section 5]), and (ii) a second-order equational logic (for specifying simple type theories), cf. [2, Part I].
If time allows, I will mention work in progress aiming at the synthesis of equational logics for specifying dependent type theories, cf. [2, Part II].
(Parts of this are joint work with my student Chung-Kil Hur.)
References
[1] Marcelo Fiore and Chung-Kil Hur. Term Equational Systems and Logics. In 24th Mathematical Foundations of Programming Semantics Conf. (MFPS XXIV), 2008. Paper
[2] Marcelo Fiore. Second-order and dependently-sorted abstract syntax. In Logic in Computer Science Conf. (LICS'08), pages 57-68. IEEE, Computer Society Press, 2008. Paper Slides
Corecursive Algebras: A Study of General Structured Corecursion
Date: Sep 16
Speaker: Tarmo Uustalu (Institute of Cybernetics in Tallinn, Estonia)
Abstract:
Dualizing the work of Osius, Taylor, and others on general structured recursion and induction in terms of recursive and wellfounded coalgebras, we study general structured corecursion and coinduction. We call an algebra of a functor corecursive, if from any coalgebra of the same functor there is a unique map to this algebra, and antifounded, if it admits a certain bisimulation principle. We show that both of these concepts are perfectly meaningful and relevant for programming and verification. However, differently from recursiveness and wellfoundedness, which are equivalent concepts under mild conditions, they are generally inequivalent. (Joint work with Venanzio Capretta and Varmo Vene.)
Mathematical Proofs in Natural Languages
Date: Jun 18
Speaker: Muhammad Humayoun (Laboratoire de Mathematiques, Universite de Savoie, France)
Abstract:
Mathematical proofs are normally written in plain natural language. Natural languages are rich, complex, and ambiguous. Having this in mind, Formal methods try to solve this problem by replacing natural languages with rich mathematical formalisms which are understood by model checkers or theorem provers. They are very precise, accurate and clear but not easily understood by Mathematicians.
A controlled natural language tries to solve this problem by taking the best to both worlds i.e. natural languages and formal languages. A controlled language is a subset of natural language whose grammar and dictionary is restricted. It helps us to reduce/eliminate ambiguity and complexity. We are developing a controlled natural language having large coverage, which (we hope) will be good enough for writing Mathematical Proofs interactively.
In this talk, I'll explain the ongoing work and implementation details.
Coq's Proof Search (somewhat) Unleashed
Date: Jun 11
Speaker: Arnaud Spiwack
Abstract:
In this talk, I will report on my work in upgrading Coq's proof engine. I will try to present some theoretical justifications of refinement as a main low-level tactics as well as reflexions on the choices I made.
The interpretation of intuitionistic type theory in locally cartesian closed categories: an intuitionistic perspective
Date: May 14
Speaker: Peter Dybjer
Abstract:
I will give an intuitionistic view of the Seely-Curien-Hofmann interpretation of Martin-Löf type in locally cartesian closed categories. The point is to use Martin-Löf type theory itself as metalanguage, and use the constructive notion of category, a so called E-category. As a categorical substitute for Martin-Löf type theory I will use E-categories with families, and discuss how to interpret such categories in E-locally cartesian closed categories. This is joint work with Alexandre Buisse, who has formalized the key part of this proof in Coq.
(This is a rehearsal for a talk I will give next week at MFPS in a special session to celebrate that Phil Scott is 60 this year.)
The experimental effectiveness of mathematical proofs
Date: May 12
Speaker: Alexandre Miquel
Abstract:
The Curry-Howard correspondence interprets each mathematical proof as a program realizing some specification (deduced from the proved formula) But what happens when the proof relies on experimental assumptions - for instance laws of physics? In this talk, I propose to study the frontier between mathematical reasoning and the empirical hypotheses underlying natural sciences. For that, I will start from a problem posed by the philosopher Karl R. Popper on the use of abstract mathematical tools in an empirical framework. I will then show how modern realizability techniques can be used to solve this problem, suggesting new ways of combining mathematical reasoning with experimental protocols effectively.
An introduction to classical realizability
Date: May 7
Speaker: Alexandre Miquel
Abstract:
In this talk I will present the basics of Jean-Louis Krivine's framework for classical realisability. First, I will present the calculus of realizers (an extension of lambda-calculus with call-cc) and its evaluation rules. Then I will define the language of second-order arithmetic and show how to define the realizability relation. Finally, I will show how to extract programs from classical proofs, and discuss the possible extensions of this theory to Zermelo-Fraenkel set theory or the calculus of constructions with universes.
Recent features in Agda (video meeting with AIST, on Wednesday at 9am (4pm in Japan))
Date: May 7
Speaker: Ulf Norell
Abstract:
I will talk about two recent features in Agda:
- Improved support for working with universes
- Haskell FFI
A Type of Partial Recursive Functions
(Joint work with Venanzio Capretta, Radboud University Nijmegen)
Date: Apr 23
Speaker: Ana Bove
Abstract:
Our goal is to define a type of partial recursive functions in constructive type theory. Previously, we studied two different formulations of partial functions and general recursion. In both cases, we could obtain a type only by extending the theory with either an impredicative universe or with coinductive definitions. Here we present a new type constructor that eludes such entities of dubious constructive credentials.
We start by showing how to break down a recursive function definition into three components: the first component generates the arguments of the recursive calls, the second one evaluates them, and the last one computes the output from the results of the recursive calls. We use this dissection as the basis for the introduction rule of the new type constructor: a partial recursive function is created by giving the first and third of the above components.
As in one of our previous methods, every partial recursive function is associated with an inductive domain predicate and evaluation of the function requires a proof that the predicate holds on the input values.
We give a constructive justification for the new construct by means of an interpretation from the extended type theory into the base one. This shows that the extended theory is consistent and constructive.
Formalizing categorical models of type theory inside type theory
Date: Apr 2
Speaker: Alexandre Buisse
Abstract:
We investigate the possible formalization of categorical metatheory of constructive type theory in (an extension of) itself, using the notion of ``internal type theory''. The model chosen is categories with families, which model the most basic part of dependent type theory. We will discuss how to formalize them inside type theory, and also how to formalize the proof that categories with finite limits, another model of type theory, can be seen as categories with families. The formalization was carried out with the proof assistant coq, and we will present it in detail.
Data, Deliberately
Date: Mar 12
Speaker: Ulf Norell
Abstract:
I'll present Conor's talk from the Dependently Typed Programming workshop in Nottingham a few weeks ago. The talk is about relationships between datatypes and the setting is a universe of first-order inductive families. As an example we will look at the relationship between lists and vectors.
Computing linguistically-based textual inferences
Date: Mar 5
Speaker: Lauri Karttunen (Palo Alto Research Center, Stanford University)
Abstract:
A long-standing goal of computational linguistics is to build a system for answering natural language questions. A successful QA system has to recognize semantic relations between sentences. If the user would like to know the answer a question such as Did Shackleton reach the South Pole?, the system should recognize that the sentence Shackleton failed to reach the South Pole contains the answer. None of the current search engines is capable of delivering a simple NO answer in such cases. The system I will describe in this talk does make the correct inference. It is the Bridge system (a bridge from language to logic) developed at the Palo Alto Research Center. The particular task the talk will focus on is entailment and contradiction detection (ECD), a more refined variant of the PASCAL RTE (Recognizing Textual Entailment) challenge. Given a passage of text and a query, does the query sentence follow from the text in the passage, is it contradicted by it, or neither? Here are examples of all three cases:
Passage: Oswald assassinated Kennedy.
Query: Did Kennedy die?
Response: YES
Passage: Bill forgot to shave this morning.
Query: Did Bill shave this morning?
Response: NO
Passage: There is a cat in the yard.
Query: Is there a black cat in the yard?
Response: UNKNOWN
The ECD algorithm operates on the level of Abstract Knowledge Structure (AKR) without the need of disambiguation. An AKR representation, derived from the syntactic and semantic analyses of a sentence, is a flat set of facts that involves concepts, roles, and contexts. Texts are parsed to produce packed syntactic representations, and these are rewritten and canonicalized, without unpacking, into AKR. Canonicalization is determined both by the structure of the representations and the lexical items involved. The system includes knowledge about words and their relations between them that are encoded in resources such as WordNet and VerbNet. It also includes knowledge about lexically or constructionally triggered presuppositions and entailments.
The ECD process first aligns context and concept terms, and then computes specificity relations between the aligned concept terms. Some special case reasoners support identification of named objects, comparison of specificity of WordNet synsets, and compatibility of cardinality restrictions. All the query facts that are entailed by the corresponding passage facts get removed. If all the query facts get eliminated, the system will respond YES. If a conflict is detected, that is, if one the aligned terms is instantiable and the other is uninstantiable, the system will respond NO. If some query facts remain at the end, the response is UNKNOWN.
The linguistic phenomena illustrated in this presentation include lexical entailments (kill => die), relations between lexical predicates or phrasal constructions and their embedded complements (forget that S => S, forget to S => not S, take the trouble to S => S, waste an opportunity to S => not S), and inferring temporal relations from temporal modifiers.
Derivation-Carrying Code using Dependent Types
Date: Feb 6
Speaker: Patrik Jansson
Abstract:
Dependent type theory is rich enough to express that a program satisfies an input/output relational specification, but it could be hard to construct the proof term. On the other hand, squiggolists know very well how to show that one relation is included in another by algebraic reasoning. We demonstrate how to encode functional and relational derivations in a dependently typed programming language. A program is coupled with an algebraic derivation from a specification, whose correctness is guaranteed by the type system.
A calculus of definitions
Date: Jan 30
Speaker: Thierry Coquand
Links: pdf
Abstract:
Environment machines, such as Landin's SECD, Krivine's call-by-name abstract machine and Leroy ZINC's machine provide ways to implement functional programming languages. Curien gave an elegant formulation of an environment calculus to reason about such machines, while Gregoire and Leroy showed how to modify them slightly to implement strong reduction (reduction under abstractions). We suggest an extension of Curien's calculus with constructors and functions defined by case and, crucially, mutual recursive definitions. We extend Gregoire and Leroy's algorithm to this calculus. We give also a (strict) denotational semantics such that a term is normalizable as soon as it has a non bottom semantics. Finally we extend this to "lazy" constructors, which should give some hint for how to extend Agda with codata types.
A preliminary presentation of the calculus can be found at www.cs.chalmers.se/~coquand/def.pdf