The Type Theory of PL/CV3

No abstract is available for this paper.

• Publication year

  1981

• Venue

  Logic of Programs

• Publication date

  1981-05-01

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1145/357233.357238
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Preemptive Scheduling of Periodic Jobs in Uniform Multiprocessor Systems

  1983cited by this paper
• Programs as Proofs: A Synopsis

  1982cited by this paper
• An Introduction to the PL/CV2 Programming Logic

  1982influential reference
• A programming logic by Robert L. Constable and Michael J. O'Donnell. Winthrop Publishers, Cambridge, Mass. 1978. 398 pp. $15.96

  1982cited by this paper
• Intensional analysis of functions and types

  1982cited by this paper
• AVID: A system for the Interactive Development of Verifiably Correct Programs

  1981cited by this paper
• Toward a Logical Thoery of Program Data

  1981cited by this paper
• Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory

  1981cited by this paper
• A Computer System for Checking Proofs

  1981cited by this paper
• Formalizing constructive mathematics: Why and how?

  1981cited by this paper
• Report on the Type Theory (V3) of the Programming Logic PL/CV3

  1980influential reference
• A survey of the project Automath

  1980cited by this paper
• Programs and types

  1980cited by this paper
• A survey of the project Automath

  1980cited by this paper
• A constructive alternative to axiomatic data type definitions

  1980cited by this paper
• Constructive Theories of Functions and Classes

  1979cited by this paper
• Edinburgh LCF: A mechanised logic of computation

  1979cited by this paper
• Edinburgh lcf: a mechanized logic of computation

  1978cited by this paper
• The Type Theoretic Interpretation of Constructive Set Theory

  1978cited by this paper
• Prolegomena to a theory of formal reasoning

  1978cited by this paper
• Data Types as Lattices

  1976cited by this paper
• About Models for Intuitionistic Type Theories and the Notion of Definitional Equality

  1975cited by this paper
• An Intuitionistic Theory of Types: Predicative Part

  1975cited by this paper
• Symposium on Automatic Demonstration

  1970cited by this paper
• Computational logic

  1949cited by this paper
• Synthesizer: A Synt.ax- Directed Programming Environment

  year unknowncited by this paper

• A cost-aware logical framework

  2021cites this paper
• Objective Metatheory of Cubical Type Theories

  2020cites this paper
• A Cubical Language for Bishop Sets

  2020cites this paper
• Generative type abstraction and type-level computation

  2011cites this paper
• The Triumph of Types : Creating a Logic of Computational Reality

  2011cites this paper
• Innovations in computational type theory using Nuprl

  2006cites this paper
• Theory and Implementation of an Efficient Tactic-Based Logical Framework

  2002cites this paper
• Programming with Types

  2002cites this paper
• Nuprl ’ s Class Theory and its Applications

  2000cites this paper
• Type-Theoretic Methodology for Practical Programming Languages

  1998cites this paper
• Decidability Extracted: Synthesizing "Correct-by-Construction" Decision Procedures form Constructive Proofs

  1998cites this paper
• Chapter X - Types in Logic, Mathematics and Programming

  1998cites this paper
• Introduction to the Literature on Programming Language Design

  1996cites this paper
• Compiling polymorphism using intensional type analysis

  1995cites this paper
• Expressing Computational Complexity in Constructive Type Theory

  1994cites this paper
• Introduction to the Literature on Semantics

  1994cites this paper
• Static Semantics, Types, and Binding Time Analysis

  1991influential citation
• How to Reconcile Subtypes, Dependent Types and Deep Polymorphism in One Language

  1991cites this paper
• Type Checking with Universes

  1991cites this paper
• Experience using type theory as a foundation for computer science

  1991cites this paper
• Introduction to PROGRESS, an Attribute Graph Grammar Based Specification Language

  1990cites this paper
• PROGRESS: A VHL-Language Based on Graph Grammars

  1990cites this paper
• Generalization from Partial Parametrization in Higher-Order Type Theory

  1989cites this paper
• Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions (Draft)

  1989cites this paper
• Type theories and object-oriented programmimg Test Nizar

  1988cites this paper
• On church's formal theory of functions and functionals: The λ-calculus: connections to higher type recursion theory, proof theory, category theory

  1988cites this paper
• Partial Objects in Type Theory

  1988cites this paper
• Towards a Computation System Based on Set Theory

  1988cites this paper
• A Polymorphic λ-calculus with Type:Type

  1986cites this paper
• A Polymorphic Lambda Calculus with Type:Type

  1986cites this paper
• Using dependent types to express modular structure

  1986influential citation
• Implementing mathematics with the Nuprl proof development system

  1986cites this paper
• Recursive Definitions in Type Theory

  1985cites this paper
• Embedding type structure in semantics

  1985cites this paper
• Proofs as programs

  1985cites this paper
• What is a Model? A Consumer's Perspective on Semantic Theory

  1985cites this paper
• Three Approaches to Type Structure

  1985cites this paper
• Ein konstruktives Typsystem für funktionale Programmiersprachen

  1984cites this paper
• Understanding Russell- A First Attempt

  1984cites this paper
• Data type proofs using Edinburgh LCF

  1984cites this paper
• Extending the Relational Database Data Model for Design Applications

  1984cites this paper
• Constructive Mathematics as a Programming Logic I: Some Principles of Theory

  1983cites this paper
• Mathematics as Programming

  1983cites this paper
• Partial functions in constructive formal theories

  1983cites this paper
• Programs as Proofs: A Synopsis

  1982cites this paper
• The Lambda-calculus: Connections to Higher Type Recursion Theory, Proof-theory, Category Theory 1

  year unknowncites this paper
• Thii problem would

  year unknowncites this paper