logique combinatoire typée

[bur...@math.jussieu.fr]

Chers tous,

Quelqu'un sait s'il existe-t-il une logique combinatoire typée qui
serait, par rapport à la logique combinatoire usuelle, l'analogue d'un
lambda calcul combinatoire typé, par rapport à celui non typé . Si
oui, j'aimerai avoir une référence?
Merci d'avance.

Amitiés
Albert

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.

[Tom Hirschowitz]

Salut Albert,

Je suis pas sur de bien comprendre ta question, mais est-ce que par
hasard la logique de Hilbert comme decrite au debut du poly de Gilles
Dowek

http://www.lix.polytechnique.fr/~dowek/Cours/theories_des_types.ps.gz

ne serait pas une reponse?

L'idee est de partir des combinateurs types

S : (a -> b -> c) -> (a -> b) -> a -> c

K : a -> b -> a

et le modus ponens.

Ca te parle?