Arrow Research search

Author name cluster

Robert L. Constable

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

13 papers
2 author rows

Possible papers

13

CSL Conference 2021 Conference Paper

Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle

  • Mark Bickford
  • Liron Cohen 0001
  • Robert L. Constable
  • Vincent Rahli

One of the differences between Brouwerian intuitionistic logic and classical logic is their treatment of time. In classical logic truth is atemporal, whereas in intuitionistic logic it is time-relative. Thus, in intuitionistic logic it is possible to acquire new knowledge as time progresses, whereas the classical Law of Excluded Middle (LEM) is essentially flattening the notion of time stating that it is possible to decide whether or not some knowledge will ever be acquired. This paper demonstrates that, nonetheless, the two approaches are not necessarily incompatible by introducing an intuitionistic type theory along with a Beth-like model for it that provide some middle ground. On one hand they incorporate a notion of progressing time and include evolving mathematical entities in the form of choice sequences, and on the other hand they are consistent with a variant of the classical LEM. Accordingly, this new type theory provides the basis for a more classically inclined Brouwerian intuitionistic type theory.

Details

LPAR Conference 2004 Conference Paper

Knowledge-Based Synthesis of Distributed Systems Using Event Structures

  • Mark Bickford
  • Robert L. Constable
  • Joseph Y. Halpern
  • Sabina Petride

Abstract To produce a program guaranteed to satisfy a given specification one can synthesize it from a formal constructive proof that a computation satisfying that specification exists. This process is particularly effective if the specifications are written in a high-level language that makes it easy for designers to specify their goals. We consider a high-level specification language that results from adding knowledge to a fragment of Nuprl specifically tailored for specifying distributed protocols, called event theory. We then show how high-level knowledge-based programs can be synthesized from the knowledge-based specifications using a proof development system such as Nuprl. Methods of Halpern and Zuck [15] then apply to convert these knowledge-based protocols to ordinary protocols. These methods can be expressed as heuristic transformation tactics in Nuprl.

Details

I&C Journal 1998 Journal Article

A Note on Complexity Measures for Inductive Classes in Constructive Type Theory

  • Robert L. Constable

It is notoriously hard to express computational complexity properties of programs in programming logics based on a semantics which respects extensional function equality. That is a serious impediment to applications of programming logics requiring reasoning about complexity. This paper shows how to use existing mechanisms to define internal computational complexity measures in logics that support inductively defined types, dependent products, and functions. The method exploits a feature of inductive definitions in constructive type theory, namely that implicit proof codes are kept with the objects showing how they are presented in the inductive class. The idea is illustrated by giving a formal inductive definition ofPTimebased on ideas from Leivant's work and on Bellantoni and Cook's approach. Then a complexity measure is defined on elements of this class. This paper discusses the limitations of this idea and the need forfaithfulnessguarantees that link internal complexity classes to the implementation of the logic. The paper concludes with a definition ofresource bounded logicsand a discussion of interesting lines of investigation of these logics which have the potential to make practical uses of results from computational complexity theory in formal reasoning about the efficiency of programs.

Details DOI

TCS Journal 1993 Journal Article

Computational foundations of basic recursive function theory

  • Robert L. Constable
  • Scott F. Smith

The theory of computability, or basic recursive function theory as it is often called, is usually motivated and developed using Church's thesis. Here we show that there is an alternative computability theory in which some of the basic results on unsolvability become more absolute, results on completeness become simpler, and many of the central concepts become more abstract. In this approach computations are viewed as mathematical objects, and theorems in recursion theory may be classified according to which axioms of computation are needed to prove them. The theory is about typed functions over the natural numbers, and it includes theorems showing that there are unsolvable problems in this setting independent of the existence of indexings. The unsolvability results are interpreted to show that the partial function concept, so important in computer science, serves to distinguish between classical and constructive type theories (in a different way than does the decidability concept as expressed in the law of excluded middle). The implications of these ideas for the logical foundations of computer science are discussed, particularly in the context of recent interest in using constructive type theory in programming.

Details DOI

FOCS Conference 1980 Conference Paper

Programs and Types

  • Robert L. Constable

The first two sections of this paper motivate and outline a constructive theory of (data) types which we developed for formal program verification. The executable component of the theory provides a very high level programming language with a rich type structure. A theory of this generality appears necessary to manage complex programming and formal reasoning about it. The logical component, influencea by AUTOMATH and LCF and based on Martin-Löf's ITT, appears strong enough to formalize constructive mathematics; hence a theory or this generality is probably sufficient for program development and verification. The last two sections of the paper illustrate the richness of the theory and the benefits of generality by describing with it different "denotational" semantics for programs. Because the theory is constructive, these abstract semantics are also computational.

Details

STOC Conference 1977 Conference Paper

On the Theory of Programming Logics

  • Robert L. Constable

A new logic for reasoning about programs is proposed here, and its metamathematics is investigated. No new primitive notions are needed for the logic beyond those used in elementary programming and mathematics, yet the combination of these notions is remarkably powerful. The logic includes a programming language, designed with Michael O'Donnell, for program verification. It forms the core of the PL/CV verifier at Cornell. This study belongs to the discipline of Algorithmic Logic as conceived by Engeler. The logic is related to Park's mu-calculus based on functions instead of relations. The monadic quantifier free subset is developed in the style of the system in J.W. deBakker's Recursive Procedures. But this logic is substantially different from either of these. It is intended to be a practical programming logic in the spirit of E. Dijkstra's calculus. This paper proves the completeness and decidability of the monadic (iterative) programming logic. It discusses the polyadic logic and the programming language briefly, and considers general models for the iterative programming logic. The polyadic logic is shown to be incomplete with respect to standard models, but complete with respect to general models.

Details

TCS Journal 1976 Journal Article

Computability concepts for programming language semantics

  • Herbert Egli
  • Robert L. Constable

This paper is about mathematical problems in programming language semantics and their influence on recursive function theory. We define a notion of computability on continuous higher types (for all types) and show its equivalence to effective operators. This resuit shows that our computable operators can model mathematically (i. e. extensionally) everything that can be done in an operational semantics. These new recursion theoretic concepts which are appropriate to semantics also allow us to construct Scott models for the λ-calculus which contain all and only computably elements. Depending on the choice of the initial cpo, our general theory yields a theory for either strictly determinate or else arbitrary non-deterministic objects (parallelism). The formal theory is developed in Part II of this paper. Part I gives motivation and comparison with related work.

Details DOI

STOC Conference 1975 Conference Paper

Computability Concepts for Programming Language Semantics

  • Herbert Egli
  • Robert L. Constable

This paper is about mathematical problems in programming language semantics and their influence on recursive function theory. We define a notion of computability on continuous higher types (for all types) and show its equivalence to effective operators. This result shows that our computable operators can model mathematically (i.e. extensionally) everything that can be done in an operational semantics. These new recursion theoretic concepts which are appropriate to semantics also allow us to construct Scott models for the λ-calculus which contain all and only computable elements. Depending on the choice of the initial cpo, our general theory yields a theory for either strictly determinate or else arbitrary non-deterministic objects (parallelism). The formal theory is developed in part II of this paper. Part I gives motivation and comparison with related work.

Details

STOC Conference 1973 Conference Paper

Type Two Computational Complexity

  • Robert L. Constable

A programming language for the partial computable functionals is used as the basis for a definition of the computational complexity of functionals (type2 functions). An axiomatic account in the spirit of Blum is then provided. The novel features of this approach are justified by applying it to problems in abstract complexity, specifically operator speed-up, and by using it to define the illusive notion of the polynomial degree of an arbitrary function. New results are obtained for these degrees.

Details
v2026.09.13