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
- [Coq-Club] The typing of total recursive functions in Coq (via the untyped Lambda calculus), Dominique Larchey-Wendling, 02/02/2017
- Re: [Coq-Club] The typing of total recursive functions in Coq (via the untyped Lambda calculus), Arnaud Spiwack, 02/04/2017
- Re: [Coq-Club] The typing of total recursive functions in Coq (via the untyped Lambda calculus), Dominique Larchey-Wendling, 02/05/2017
- Re: [Coq-Club] The typing of total recursive functions in Coq (via the untyped Lambda calculus), Gaetan Gilbert, 02/06/2017
- Re: [Coq-Club] The typing of total recursive functions in Coq (via the untyped Lambda calculus), Dominique Larchey-Wendling, 02/06/2017
- Re: [Coq-Club] The typing of total recursive functions in Coq (via the untyped Lambda calculus), Matthieu Sozeau, 02/06/2017
- Re: [Coq-Club] The typing of total recursive functions in Coq (via the untyped Lambda calculus), Dominique Larchey-Wendling, 02/07/2017
- Re: [Coq-Club] The typing of total recursive functions in Coq (via the untyped Lambda calculus), Matthieu Sozeau, 02/06/2017
- Re: [Coq-Club] The typing of total recursive functions in Coq (via the untyped Lambda calculus), Dominique Larchey-Wendling, 02/06/2017
- Re: [Coq-Club] The typing of total recursive functions in Coq (via the untyped Lambda calculus), Gaetan Gilbert, 02/06/2017
- Re: [Coq-Club] The typing of total recursive functions in Coq (via the untyped Lambda calculus), Dominique Larchey-Wendling, 02/05/2017
- Re: [Coq-Club] The typing of total recursive functions in Coq (via the untyped Lambda calculus), Arnaud Spiwack, 02/04/2017
Archive powered by MHonArc 2.6.18.