HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

A Few Remarks on SKInT

Abstract : SKIn and SKInT are two first-order languages that have been proposed recently by Healfdene Goguen and the author. While SKIn encodes lambda-calculus reduction faithfully, standardizes and is confluent even on open terms, it normalizes only weakly in the simply-typed case. On the other hand, SKInT normalizes strongly in the simply-typed case, standardizes and is confluent on open terms, and also encodes lambda-calculus reduction faithfully, although in a less direct way. This report has two goals. First, we show that the natural simple type system for SKInT, seen as a natural deduction system, is not exactly a proof system for intuitionistic logic, but for a very close fragment of the modal logic S4, in which intuitionistic logic is easily coded. This explains why the SKIn and SKInT typing rules are different, and why SKInT encodes lambda-calculus in a less direct way than SKIn. Second, we show that SKInT, like $\lambda\upsilon$ and a few other calculi of explicit substitutions, preserves strong normalization. In fact, SKInT also preserves weak normalization and solvability. We show this as a corollary of a stronger result, analogous to a well-known result in the lambda-calculus: the solvable SKInT-terms are exactly those that are typable in the system $S\omega$ of conjunctive types (inspired from Émilie Sayag), the weakly normalizing SKInT-terms (with or without $\eta$) are exactly those that have a definite positive $S\omega$-typing, and the strongly normalizing SKInT-terms (with or without $\eta$) are exactly those that are typable in the system $S$ of conjunctive types, which does not have the universal type $\omega$.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 12:12:54 PM
Last modification on : Thursday, February 3, 2022 - 11:18:33 AM
Long-term archiving on: : Sunday, April 4, 2010 - 9:45:22 PM


  • HAL Id : inria-00073214, version 1



Jean Goubault-Larrecq. A Few Remarks on SKInT. [Research Report] RR-3475, INRIA. 1998. ⟨inria-00073214⟩



Record views


Files downloads