NDLI: Pure subtype systems

Please wait, while we are loading the content...

Reconfigurable asynchronous logic automata: (RALA)

On the verification problem for weak memory models

Compositional may-must program analysis: unleashing the power of alternation

A simple, verified validator for software pipelining

Dependent types from counterexamples

From Boolean to quantitative notions of correctness

Nominal system T

Decision procedures for algebraic data types with abstractions

Toward a verified relational database management system

Dependent types and program equivalence

From program verification to program synthesis

Contracts made manifest

Generating compiler optimizations from proofs

Paralocks: role-based information flow control and beyond

Nested interpolants

Coarse-grained transactions

Continuity analysis of programs

A verified compiler for an impure functional language

Low-level liquid types

A theory of indirection via approximation

Automatic numeric abstractions for heap-manipulating programs

Counterexample-guided focus

Pure subtype systems

Abstraction-guided synthesis of synchronization

Threesomes, with and without blame

Automatically generating instruction selectors using declarative machine descriptions

Modular verification of security protocol code by typing

Monads in action

Sequential verification of serializability

Program analysis via satisfiability modulo path programs

Verified just-in-time compiler on x86

Type inference for datalog with complex type hierarchies

A relational modal logic for higher-order stateful ADTs

Static determination of quantitative resource usage for higher-order programs

Structuring the verification of heap-manipulating programs

Modular session types for distributed object-oriented programming

Programming with angelic nondeterminism

Integrating typed and untyped code in a scripting language

Semantics and algorithms for data-dependent grammars

Dynamically checking ownership policies in concurrent c/c++ programs

Higher-order multi-parameter tree transducers and recursion schemes for program verification

Pure subtype systems

Content Provider	ACM Digital Library
Author	Hutchins, DeLesley S.
Abstract	This paper introduces a new approach to type theory called pure subtype systems . Pure subtype systems differ from traditional approaches to type theory (such as pure type systems) because the theory is based on subtyping, rather than typing. Proper types and typing are completely absent from the theory; the subtype relation is defined directly over objects. The traditional typing relation is shown to be a special case of subtyping, so the loss of types comes without any loss of generality. Pure subtype systems provide a uniform framework which seamlessly integrates subtyping with dependent and singleton types. The framework was designed as a theoretical foundation for several problems of practical interest, including mixin modules, virtual classes, and feature-oriented programming. The cost of using pure subtype systems is the complexity of the meta-theory. We formulate the subtype relation as an abstract reduction system, and show that the theory is sound if the underlying reductions commute. We are able to show that the reductions commute locally, but have thus far been unable to show that they commute globally. Although the proof is incomplete, it is ``close enough'' to rule out obvious counter-examples. We present it as an open problem in type theory.
Starting Page	287
Ending Page	298
Page Count	12
File Format	PDF
ISBN	9781605584799
DOI	10.1145/1706299.1706334
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2010-01-17
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Dependent types Abstract reduction systems Singleton types Subtyping Transitivity elimination
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Pure subtype systems

Dependent type system with subtyping -- type level transitivity elimination (1996).

Dependent type system with subtyping (I) type level transitivity elimination

Programming with first-class modules in a core language with subtyping, singleton kinds and open existential types

Singleton types here, singleton types there, singleton types everywhere

Dependent Types With Subtyping and Late-Bound Overloading (1999)

Dependent types with subtyping and late-bound overloading (1999).

Subtyping dependent types (2000).

Coercive subtyping for the calculus of constructions

Pure subtype systems

Similar Documents

Pure subtype systems

Dependent type system with subtyping -- type level transitivity elimination (1996).

Dependent type system with subtyping (I) type level transitivity elimination

Programming with first-class modules in a core language with subtyping, singleton kinds and open existential types

Singleton types here, singleton types there, singleton types everywhere

Dependent Types With Subtyping and Late-Bound Overloading (1999)

Dependent types with subtyping and late-bound overloading (1999).

Subtyping dependent types (2000).

Coercive subtyping for the calculus of constructions

Pure subtype systems