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

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,854

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

Explicit mathematics: power types and overloading.Thomas Studer - 2005 - Annals of Pure and Applied Logic 134 (2-3):284-302.
On the adequacy of representing higher order intuitionistic logic as a pure type system.Hans Tonino & Ken-Etsu Fujita - 1992 - Annals of Pure and Applied Logic 57 (3):251-276.
Several notes on the power of Gomory–Chvátal cuts.Edward A. Hirsch & Arist Kojevnikov - 2006 - Annals of Pure and Applied Logic 141 (3):429-436.
Imperative programs as proofs via game semantics.Martin Churchill, Jim Laird & Guy McCusker - 2013 - Annals of Pure and Applied Logic 164 (11):1038-1078.
Kripke semantics and proof systems for combining intuitionistic logic and classical logic.Chuck Liang & Dale Miller - 2013 - Annals of Pure and Applied Logic 164 (2):86-111.
Combining type disciplines.Felice Cardone, Mariangiola Dezani-Ciancaglini & Ugo de'Liguoro - 1994 - Annals of Pure and Applied Logic 66 (3):197-230.
Classical Fω, orthogonality and symmetric candidates.Stéphane Lengrand & Alexandre Miquel - 2008 - Annals of Pure and Applied Logic 153 (1-3):3-20.
Completeness and partial soundness results for intersection and union typing for λ ¯ μ μ ̃.Steffen van Bakel - 2010 - Annals of Pure and Applied Logic 161 (11):1400-1430.
Core Type Theory.Emma van Dijk, David Ripley & Julian Gutierrez - 2023 - Bulletin of the Section of Logic 52 (2):145-186.

Analytics

Added to PP
2014-01-16

Downloads
25 (#889,993)

6 months
7 (#740,041)

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