System ST toward a type system for extraction and proofs of programs

Annals of Pure and Applied Logic 122 (1-3):107-130 (2003)
  Copy   BIBTEX

Abstract

We introduce a new type system called “System ST” , based on subtyping, and prove the basic property of the system. We show the extraordinary expressive power of the system which leads us to think that it could be a good candidate for doing both proof and extraction of programs

Categories

Keywords

Reprint years

DOI

10.1016/s0168-0072(03)00002-2

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,928

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

On the philosophical significance of consistency proofs.Michael D. Resnik - 1974 - Journal of Philosophical Logic 3 (1/2):133 - 147.
Storage Operators and ∀‐positive Types in TTR Type System.Karim Nour - 1996 - Mathematical Logic Quarterly 42 (1):349-368.
Complete infinitary type logics.J. W. Degen - 1999 - Studia Logica 63 (1):85-119.
Implicit Proofs.Jan Krajíček - 2004 - Journal of Symbolic Logic 69 (2):387 - 397.
TULSI: an NLP system for extracting legal modificatory provisions. [REVIEW]Leonardo Lesmo, Alessandro Mazzei, Monica Palmirani & Daniele P. Radicioni - 2013 - Artificial Intelligence and Law 21 (2):139-172.
Term extraction and Ramsey's theorem for pairs.Alexander P. Kreuzer & Ulrich Kohlenbach - 2012 - Journal of Symbolic Logic 77 (3):853-895.
Goal-Driven Reasoning in First-Order Logic.Claes Strannegård - 2006 - In Björn Haglund & Helge Malmgren (eds.), Kvantifikator för en Dag. Essays dedicated to Dag Westerståhl on his sixtieth birthday. Philosophical Communications.
The proofs of α→α in P - W.Sachio Hirokawa - 1996 - Journal of Symbolic Logic 61 (1):195-211.
A construction of non-well-founded sets within Martin-löf's type theory.Ingrid Lindström - 1989 - Journal of Symbolic Logic 54 (1):57-64.
Mixed logic and storage operators.Karim Nour - 2000 - Archive for Mathematical Logic 39 (4):261-280.
Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalizing.Steffen van Bakel - 2004 - Notre Dame Journal of Formal Logic 45 (1):35-63.
Proofs of miracles and miracles as proofs.Richard L. Purtill - 1976 - Christian Scholar’s Review 6.

Analytics

Added to PP
2014-01-16

Downloads
17 (#868,989)

6 months
7 (#430,392)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

A formulation of the simple theory of types.Alonzo Church - 1940 - Journal of Symbolic Logic 5 (2):56-68.
A new type assignment for λ-terms.M. Coppo & M. Dezani-Ciancaglini - 1978 - Archive for Mathematical Logic 19 (1):139-156.

Add more references