I-Types of System F
Logic
2009-05-05 v1
Authors:
Karim Nour
Abstract
We prove in this paper that the types of system F inhabited uniquely by ?I-terms (the I-types) have a positive quantifier. We give also consequences of this result and some examples.
Cite
@article{arxiv.0905.0458,
title = {I-Types of System F},
author = {Karim Nour},
journal= {arXiv preprint arXiv:0905.0458},
year = {2009}
}
Related papers
View all related →
Logic · Mathematics
Un R\'esultat de Compl\'etude pour les Types $\forall^+$ du Syst\`eme F
Karim Nour, Samir Farkh
2015-05-13
Logic · Mathematics
Les types de donn\'ees syntaxiques du syst\`eme F
Samir Farkh, Karim Nour
2009-05-07
Programming Languages · Computer Science
Qualifying System F-sub
Edward Lee, Yaoyu Zhao, James You, Kavin Satheeskumar +2
2024-02-27
Logic in Computer Science · Computer Science
Polymorphic System I
Cristian F. Sottile, Alejandro Díaz-Caro, Pablo E. Martínez López
2021-07-28
Logic in Computer Science · Computer Science
Definite Descriptions in Intuitionist Positive Free Logic
Nils Kürbis
2021-08-12
Logic in Computer Science · Computer Science
Unifying type systems for mobile processes
Emmanuel Beffara
2015-05-29
Logic in Computer Science · Computer Science
The Yoneda Reduction of Polymorphic Types (Extended Version)
Paolo Pistone, Luca Tranchini
2020-11-02
Logic · Mathematics
Fixed Sets of Automorphisms of Countable, Arithmetically Saturated Structures
James H. Schmerl
2022-11-18
Logic in Computer Science · Computer Science
Combining Inclusion Polymorphism and Parametric Polymorphism
Sabine Glesner, Karl Stroetmann
2007-05-23
Logic in Computer Science · Computer Science
Practical Subtyping for System F with Sized (Co-)Induction
Rodolphe Lepigre, Christophe Raffalli
2017-07-12
Logic · Mathematics
Lawvere theories and C-systems
Vladimir Voevodsky
2015-12-29
Artificial Intelligence · Computer Science
The probatilistic Quantifier Fuzzification Mechanism FA: A theoretical analysis
Felix Diaz-Hermida, Alberto Bugarin, David E. Losada
2014-10-28
Functional Analysis · Mathematics
Unique Solutions to Power-Transformed Affine Systems
John Stachurski, Ole Wilms, Junnan Zhang
2022-12-02
Category Theory · Mathematics
Axiomatizing complete positivity
Oscar Cunningham, Chris Heunen
2015-11-06
Logic in Computer Science · Computer Science
Pure Type Systems without Explicit Contexts
Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk
2010-09-16
Logic in Computer Science · Computer Science
Internalized realizability in pure type systems
Marc Lasson
2011-08-02
Complex Variables · Mathematics
Uniformly perfect analytic and conformal non-autonomous attractor sets
Kurt Falk, Rich Stankewitz
2021-01-28
Programming Languages · Computer Science
Ill-Typed Programs Don't Evaluate
Steven Ramsay, Charlie Walpole
2023-10-23
Group Theory · Mathematics
Type systems and maximal subgroups of Thompson's group $V$
James Belk, Collin Bleak, Martyn Quick, Rachel Skipper
2024-02-28
Logic · Mathematics
Constructive Quantifier Elimination with a Focus on Matrix Rings
Maximilian Illmer, Tim Netzer
2025-03-25
General Topology · Mathematics
Very I-favorable spaces
A. Kucharski, Sz. Plewik, V. Valov
2010-11-17
Logic in Computer Science · Computer Science
Extensional proofs in a propositional logic modulo isomorphisms
Alejandro Díaz-Caro, Gilles Dowek
2023-09-19
Spectral Theory · Mathematics
Power series with positive coefficients arising from the characteristic polynomials of positive matrices
Thomas J. Laffey, Raphael Loewy, Helena Šmigoc
2013-07-18
Logic in Computer Science · Computer Science
A formalization of System I with type Top in Agda
Agustín Séttimo, Cristian Sottile, Cecilia Manzino
2026-03-26
Representation Theory · Mathematics
A Positive Quantization on Type I Locally Compact Groups
Marius Mantoiu
2015-12-07