[go: up one dir, main page]

Wells, 1999 - Google Patents

Typability and type checking in System F are equivalent and undecidable

Wells, 1999

View PDF
Document ID
8416639604773915621
Author
Wells J
Publication year
Publication venue
Annals of Pure and Applied Logic

External Links

Snippet

Girard and Reynolds independently invented System F (aka the second-order polymorphically typed lambda calculus) to handle problems in logic and computer programming language design, respectively. Viewing F in the Curry style, which associates …
Continue reading at www.sciencedirect.com (PDF) (other versions)

Classifications

    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/40—Transformations of program code
    • G06F8/41—Compilation
    • G06F8/43—Checking; Contextual analysis
    • G06F8/436—Semantic checking
    • G06F8/437—Type checking
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/40—Transformations of program code
    • G06F8/41—Compilation
    • G06F8/42—Syntactic analysis
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/30—Creation or generation of source code
    • G06F8/31—Programming languages or programming paradigms
    • G06F8/315—Object-oriented languages
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/20—Handling natural language data
    • G06F17/27—Automatic analysis, e.g. parsing
    • G06F17/2705—Parsing
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/44—Arrangements for executing specific programmes
    • G06F9/4421—Execution paradigms
    • G06F9/4428—Object-oriented
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3604—Software analysis for verifying properties of programs
    • G06F11/3608—Software analysis for verifying properties of programs using formal methods, e.g. model checking, abstract interpretation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G06F11/3668—Software testing
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/70—Software maintenance or management
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/10—Requirements analysis; Specification techniques
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/30—Information retrieval; Database structures therefor; File system structures therefor
    • G06F17/30943—Information retrieval; Database structures therefor; File system structures therefor details of database functions independent of the retrieved data type
    • G06F17/30946—Information retrieval; Database structures therefor; File system structures therefor details of database functions independent of the retrieved data type indexing structures
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity

Similar Documents

Publication Publication Date Title
Wells Typability and type checking in System F are equivalent and undecidable
Sannella et al. Foundations of algebraic specification and formal software development
Sutter Exceptional C++: 47 engineering puzzles, programming problems, and solutions
Bardohl et al. Integrating meta-modelling aspects with graph transformation for efficient visual language definition and model manipulation
Nugues An introduction to language processing with Perl and Prolog: an outline of theories, implementation, and application with special consideration of English, French, and German
Fernández Models of computation: an introduction to computability theory
Jay Pattern Calculus: Computing with Functions and Structures
Blume et al. Sound and complete models of contracts
Tsukada et al. Compositional higher-order model checking via ω-regular games over Böhm trees
Bakema et al. Fully communication oriented NIAM
Kiselyov Effects Without Monads: Non-determinism--Back to the Meta Language
Tuerk A separation logic framework for HOL
Berglund et al. Shuffled languages—Representation and recognition
Huggins The static and dynamic semantics of C
Colby Semantics-based Program Analysis via Symbolic Composition of Transfer Relations
Murray Recursive types for cogent
Hemmerling Computability of String Functions Over Algebraic Structures Armin Hemmerling
Attiogbé Semantic embedding of Petri nets into Event-B
Matthews et al. An operational semantics for R5RS Scheme
Tejiščák Erasure in dependently typed programming
Banach et al. A Translation of the Pi-Calculus into MONSTR
Hussain et al. temporaljmlc: A jml runtime assertion checker extension for specification and checking of temporal properties
Shengyi Mechanized Verification of Graph-Manipulating Programs
Feldman Teaching quality object-oriented programming
Visser The Stratego Reference Manual