Skip to Content.
Sympa Menu

coq-club - [Coq-Club] The typing of total recursive functions in Coq (via the untyped Lambda calculus)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] The typing of total recursive functions in Coq (via the untyped Lambda calculus)


Chronological Thread 
  • From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] The typing of total recursive functions in Coq (via the untyped Lambda calculus)
  • Date: Thu, 2 Feb 2017 16:18:04 +0100
  • Organization: LORIA

Dear Coq users,

I am happy to announce the availability of a dependently typed
implementation of the untyped Lambda Calculus in Coq.

http://www.loria.fr/~larchey/Lambda_Calculus

One of the by-products of that development is a formal proof
that:

Every total recursive function f : N -> N can be represented by
Coq term tf : nat -> nat (which can be computed from the algorithm
that describes f.) (*)

Of course the problem is to circumvent the unbounded minimization
scheme. I know that there have been many published (and unpublished)
implementations of the untyped Lambda Calculus.

This one enjoys the following properties:

1/ A dependently typed representation of terms which avoids the problem
induced by alpha conversion: two alpha-equivalent terms are equal.
The type of terms is parametrized by the number of usable free
variables.

2/ Most of the proofs of JL Krivine's book "Lambda-Calculus: Types and
Models" are implemented in an intuitionistic way (no axiom is used).
Intersection types system D and Domega are implemented with the
characterization of strongly normalizable terms.

System F is not implemented yet though (but this is not really
the goal of this project).

3/ A dependently typed representation of recursive algorithm and
a formal proof of the encoding of recursive algorithm by untyped
lambda terms.

The main objective of this project is to build a Coq library
that could be used to implement *undecidability results*
(for various logics) in an intuitionistic way.

The development is ongoing on my private repository but anyone
interested in such a project can be given access to that
development branch. Do not hesitate to contact me.

Dominique Larchey-Wendling
TYPES, LORIA, CNRS

(*) the word "total" which could be ambiguous (as it refers to
meta-theory), should here be understood as "provably total" in Coq



Archive powered by MHonArc 2.6.18.

Top of Page