Proposal for a natural formalization of functional programming concepts
Reducibility method in simply typed lambda calculus.
Representación grafica del teorema de Church y Rosser
Rétractions et interprétation interne du polymorphisme : le problème de la rétraction universelle
Right and left invertibility in -calculus
Semantic analysis of topic and focus
Sémantique catégorique des types : comprendre le système F
Sémantique formelle des opérateurs d'un langage de listes
Set theory in predicate calculus with equality
Sober spaces and continuations.
Some generalizations to two systems of set theory based on combinatory logic.
Some remarks about the connections between combinatory logic and axiomatic recursion theory.
Sur les éléments de construction de la logique mathématique
Il s'agit de présenter l'article de Schönfinkel «Über die Bausteine der mathematischen Logik», préparé pour la publication (1924) par H. Behmann, d'après une conférence de Schönfinkel en 1920, qui fonde ce que Curry nommera «la logique combinatoire». L'objectif principal du travail de Schönfinkel est l'élimination générale des variables (propositionnelles, prédicatives, individuelles), grâce à l'usage de plusieurs «fonctions particulières». On trouvera ici : (1) une introduction à l'article de Schönfinkel,...
The maximality of the typed lambda calculus and of cartesian closed categories
Théorème de Church-Rosser et structuration des langues naturelles
Two extensions of system F with (co)iteration and primitive (co)recursion principles
This paper presents two extensions of the second order polymorphic lambda calculus, system F, with monotone (co)inductive types supporting (co)iteration, primitive (co)recursion and inversion principles as primitives. One extension is inspired by the usual categorical approach to programming by means of initial algebras and final coalgebras; whereas the other models dialgebras, and can be seen as an extension of Hagino's categorical lambda calculus within the framework of parametric polymorphism....
Un modèle fonctionnel des structures de contrôle
Une généralisation de la théorie des types en -calcul
Une généralisation de la théorie des types en -calcul (II)
О выразимости функционалов в языке Д.Скотта LCF