NDLI: Logical types for untyped languages

Content Provider	ACM Digital Library
Author	Tobin-Hochstadt, Sam Felleisen, Matthias
Abstract	Programmers reason about their programs using a wide variety of formal and informal methods. Programmers in untyped languages such as Scheme or Erlang are able to use any such method to reason about the type behavior of their programs. Our type system for Scheme accommodates common reasoning methods by assigning variable occurrences a subtype of their declared type based on the predicates prior to the occurrence, a discipline dubbed occurrence typing. It thus enables programmers to enrich existing Scheme code with types, while requiring few changes to the code itself. Three years of practical experience has revealed serious shortcomings of our type system. In particular, it relied on a system of ad-hoc rules to relate combinations of predicates, it could not reason about subcomponents of data structures, and it could not follow sophisticated reasoning about the relationship among predicate tests, all of which are used in existing code. In this paper, we reformulate occurrence typing to eliminate these shortcomings. The new formulation derives propositional logic formulas that hold when an expression evaluates to true or false, respectively. A simple proof system is then used to determine types of variable occurrences from these propositions. Our implementation of this revised occurrence type system thus copes with many more untyped programming idioms than the original system.
Starting Page	117
Ending Page	128
Page Count	12
File Format	MOBI / PRC EPUB PDF QT / MOV
ISSN	03621340 15581160
DOI	10.1145/1932681.1863561
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	45
Issue Number	9
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1983-05-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Type systems Logic Untyped languages
Content Type	Video Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Software

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

Logical types for untyped languages

Practical affine types

Linear dependent types for differential privacy

Dependent Information Flow Types

Functors are Type Refinement Systems

Nested refinements:a logic for duck typing

Superficially substructural types

Polymorphic type inference for scripting languages with object extensions

Refined types: highly differentiated type systems and their use in the design of intermediate languages

Logical types for untyped languages

Similar Documents

Logical types for untyped languages

Practical affine types

Linear dependent types for differential privacy

Dependent Information Flow Types

Functors are Type Refinement Systems

Nested refinements:a logic for duck typing

Superficially substructural types

Polymorphic type inference for scripting languages with object extensions

Refined types: highly differentiated type systems and their use in the design of intermediate languages

Logical types for untyped languages