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.

Powerful yet effective induction principles play an important role in computing, being a paramount component of programming languages, automated reasoning, and program verification systems. The Bar Induction (BI) principle is a fundamental concept of intuitionism, which is equivalent to the standard principle of transfinite induction. In this work, we investigate the compatibility of several variants of BI with Constructive Type Theory (CTT), a dependent type theory in the spirit of Martin-Löf’s extensional theory. We first show that CTT is compatible with a BI principle for sequences of numbers. Then, we establish the compatibility of CTT with a more general BI principle for sequences of name-free closed terms. The formalization of the latter principle within the theory involved enriching CTT’s term syntax with a limit constructor and showing that consistency is preserved. Furthermore, we provide novel insights regarding BI, such as the non-truncated version of BI on monotone bars being intuitionistically false. These enhancements are carried out formally using the Nuprl proof assistant that implements CTT and the formalization of CTT within the Coq proof assistant presented in previous works.

Abstract In this article we define pure intuitionistic Ancestral Logic ( iAL ), extending pure intuitionistic First-Order Logic ( iFOL ). This logic is a dependently typed abstract programming language with computational functionality beyond iFOL given by its realizer for the transitive closure, TC . We derive this operator from the natural type theoretic definition of TC using intersection. We show that provable formulas in iAL are uniformly realizable, thus iAL is sound with respect to constructive type theory. We further show that iAL subsumes Kleene Algebras with tests and thus serves as a natural programming logic for proving properties of program schemes. We also extract schemes from proofs that iAL specifications are solvable.

Church-Turing computability was extended by Brouwer who considered non-lawlike computability in the form of free choice sequences. Those are essentially unbounded sequences whose elements are chosen freely, i.e. not subject to any law. In this work we develop a new type theory BITT, which is an extension of the type theory of the Nuprl proof assistant, that embeds the notion of choice sequences. Supporting the evolving, non-deterministic nature of these objects required major modifications to the underlying type theory. Even though the construction of a choice sequence is non-deterministic, once certain choices were made, they must remain consistent. To ensure this, BITT uses the underlying library as state and store choices as they are created. Another salient feature of BITT is that it uses a Beth-like semantics to account for the dynamic nature of choice sequences. We formally define BITT and use it to interpret and validate essential axioms governing choice sequences. These results provide a foundation for a fully intuitionistic version of Nuprl.

We present an extension of the computation system and logic of the Nuprl proof assistant with intuitionistic principles, namely versions of Brouwer's bar induction principle, which is equivalent to transfinite induction. We have substantially extended the formalization of Nuprl's type theory within the Coq proof assistant to show that two such bar induction principles are valid w.r.t. Nuprl's semantics (the Good): one for sequences of numbers that involved only minor changes to the system, and a more general one for sequences of name-free (the Ugly) closed terms that involved adding a limit constructor to Nuprl's term syntax in our model of Nuprl's logic. We have proved that these additions preserve Nuprl's key metatheoretical properties such as consistency. Finally, we show some new insights regarding bar induction, such as the non-truncated version of bar induction on monotone bars is intuitionistically false (the Bad).

Fault-tolerant distributed systems often contain complex error handling code. Such code is hard to test or model-check because there are often too many possible failure scenarios to consider. As we will demonstrate in this paper, formal methods have evolved to a state in which it is possible to generate this code along with correctness guarantees. This paper describes our experience with building highly-available databases using replication protocols that were generated with the help of correct-by-construction formal methods. The goal of our project is to obtain databases with unsurpassed reliability while providing good performance. We report on our experience using a total order broadcast protocol based on Paxos and specified using a new formal language called Event ML. We compile Event ML specifications into a form that can be formally verified while simultaneously obtaining code that can be executed. We have developed two replicated databases based on this code and show that they have performance that is competitive with popular databases in one of the two considered benchmarks.

We present a fault-tolerant ordered broadcast service that is correct-by-construction. Our broadcast service allows for diversity in space, whereby the participants in the broadcast protocol run different code, as well as in time, whereby the protocol itself is changed periodically. We use the Nuprl proof assistant to specify the service, prove correctness, and synthesize the code. The paper includes initial performance results.

In this article I will examine a few key concepts and design decisions that account for the high value of implemented constructive type theories in computer science. I'll stress the historical fact that these theories, and the proof assistants that animate them, were born from a strong partnership linking computer science, logic, and mathematics. I will recall how modern type theory researchers built on deep insights from the earliest pioneers: Turing - the first computer scientist, Church - the patriarch of logic in computer science, and Brouwer - a singular pioneer of intuitionism and constructive mathematics. They created solid intellectual ground on which to build a formal implemented constructive theory of computation whose influence will be felt well beyond computing and information science alone. All generations of constructive type theory researchers since this beginning have had leaders from all three disciplines. Much of the seminal modern work creating these type theories and their proof assistants was presented in LICS proceedings, and LICS could be a natural home for future work in this flourishing area which is the epitome of logic in computer science.

Church's Higher Order Logic is a basis for influential proof assistants -- HOL and PVS. Church's logic has a simple set-theoretic semantics, making it trustworthy and extensible. We factor HOL into a constructive core plus axioms of excluded middle and choice. We similarly factor standard set theory, ZFC, into a constructive core, IZF, and axioms of excluded middle and choice. Then we provide the standard set-theoretic semantics in such a way that the constructive core of HOL is mapped into IZF. We use the disjunction, numerical existence and term existence properties of IZF to provide a program extraction capability from proofs in the constructive core. We can implement the disjunction and numerical existence properties in two different ways: one using Rathjen's realizability for IZF and the other using a new direct weak normalization result for IZF by Moczydlowski. The latter can also be used for the term existence property.

Although building systems from components has attractions, this approach also has problems. Can we be sure that a certain configuration of components is correct? Can it perform as well as a monolithic system? Our paper answers these questions for the Ensemble communication architecture by showing how, with help of the Nuprl formal system, configurations may be checked against specifications, and how optimized code can be synthesized from these configurations. The performance results show that we can substantially reduce end-to-end latency in the already optimized Ensemble system. Finally, we discuss whether the techniques we used are general enough for systems other than communication systems.

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.

Type theory is an elegant organisation of the fundamental principles of a foundational theory of computing, with theory taken in the sense of a scientific theory as well as a deductive theory. This theory generates a research programme. I examine the elements of this programme and assess progress. A large number of people world wide have been pursuing the type theory aspects of this research programme, so we can survey a large body of work created over a 20 year period for hints of success and failure and challenge. I first look at a few successes. Some of the applications we have attempted have not worked out as expected, and we don't know whether the fault lies with the type theory or elsewhere. I first describe a failure that is clearly not the type theory, but the state of the foundations of computational mathematics. Then we look at problems closer to the structure of modern type theories-problems suggested by the success of classical set theory.

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.

The authors lay the foundations for reasoning about proofs whose steps include both invocations of programs to build subproofs (tactics) and references to representations of proofs themselves (reflected proofs). The main result is the definition of a single type of proof which can mention itself, using a novel technique which finds a fixed point of a mapping between metalanguage and object language. This single type contrasts with hierarchies of types used in other approaches to accomplish the same classification. It is shown that these proofs are valid, and that every proof can be reduced to a proof involving only primitive inference rules. The extension of the results to proofs from which programs (such as tactics) can be derive and to proofs that can refer to a library of definitions and previously proven theorems is shown. It is believed that the mechanism of reflection is fundamental in building proof development systems, and its power is illustrated with applications to automating reasoning and describing modes of computation.>

The theory of computability often called basic recursive function theory is usually motivated and developed using Church's thesis. It is shown 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 the major theorems in recursion theory may be classified according to which axioms about computation are needed to prove them. The theory is a typed theory of functions over the natural numbers, and 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 serves to distinguish between classical and constructive type theories.>

The significant intellectual cost of programming is for problem solving and explaining, not for coding. Yet programming systems offer mechanical assistance for the coding process exclusively. We illustrate the use of an implemented program development system, called PRL ("pearl"), that provides automated assistance with the difficult part. The problem and its explained solution are seen as formal objects in a constructive logic of the data domains. These formal explanations can be executed at various stages of completion. The most incomplete explanations resemble applicative programs, the most complete are formal proofs.

article Free Access Share on The Type Theory of PL/CV3 Authors: Robert L. Constable Department of Computer Science, 405 Upson Hall, Cornell University, Ithaca, N.Y. Department of Computer Science, 405 Upson Hall, Cornell University, Ithaca, N.Y.View Profile , Daniel R. Zlatin Department of Computer Science, 405 Upson Hall, Cornell University, Ithaca, N.Y. Department of Computer Science, 405 Upson Hall, Cornell University, Ithaca, N.Y.View Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 6Issue 1Jan. 1984 pp 94–117https://doi.org/10.1145/357233.357238Online:01 January 1984Publication History 25citation305DownloadsMetricsTotal Citations25Total Downloads305Last 12 Months12Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

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.

The computatiional complexity of several decidable problems about program schemes, recursion schemes, and simple programming languages is considered. The strong equivalence, weak equivalence, containment, halting, and divergence problems for the single variable program schemes and the linear monadic recursion schemes are shown to be $NP$-complete. The equivalence problem for the Loop 1 programming language is also shown to be $NP$-complete. Sufficient conditions for a program scheme problem to be $NP$-hard are presented. The strong equivalence problem for a subset of the single variable program schemes, the strongly free schemes, is shown to be decidable deterministically in polynomial time.

PL/CV is a new formal system which mixes commands and assertions. It includes axioms and rules for a theory of programming over integers and characters. Since arguments in the theory can be checked by the PL/CV Proof Checker, the system offers an approach to mechanical program verification. The Proof Checker is efficient enough for classroom use. Early experience with PL/CV indicates that it nicely supports formal verification of elementary arguments. Continued work should enable the formalization of non-elementary reasoning as well.

We describe a means of presenting hierarchically organized formal definitions of programming languages using the denotational approach of D. Scott and C. Strachey. As an example of our approach, we give the semantics of PL/CS, an instructional variant of PL/I. We also discuss the implications of this approach to language design, pointing out some cases where the wrong choices may cause the hierarchy to collapse into chaotic rubble.

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.

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).

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.

The study of program schemata and the study of subrecursive programming languages are both concerned with limiting program structure in order to permit a more complete analysis of algorithms while retaining sufficiently rich computing power to allow interesting algorithms. In this paper we combine these approaches by defining classes of subrecursive program schemata and investigating their equivalence problems. Since the languages are all subrecursive, any scheme written in any one of them must halt (as long as we assume the basic functions and predicates are all total). Hence equivalence of schemes is the first question of interest we can ask about these languages.

Ansra.~cr.One of the central problems in the study of computational complexity has been to determine those changes in computing resource sufficient to allow a computing system to do more work.Our main theorem affirms that no total effective operator ~s sufficient to increase every recursive resource bound to the point of getting more work from the system.This result is an extension of the gap theorem discovered by Borodin for the composition operator, and it confirms the fact that the "gap" is an intrinsic property of computational complexity measures.The proofs in the paper are constructively (even intuitionistically) valid.

The structural complexity of programming languages, and therefore of programs as well, can be measured by the subrecursive class of functions which characterize the language.Using such a measure of structural complexity, we examine the trade-off relationship between structural and computational complexity.Since measures of structural complexity directly related to high level languages interest us most, we use abstract language models which approximate highly structured languages like Algol.

We define the following classes of program schemata: ${\text{P}} = $ class of schemes using a finite number of simple variables; ${\text{P}}_{\text{A}} = $ class of schemes using simple and subscripted variables (arrays); ${\text{P}}_{{\text{Ae}}} = $ class of schemes in ${\text{P}}_{\text{A}} = $, with the addition of an equality test on subscript values; ${\text{P}}_{\text{R}} = $ class of schemes allowing recursive functions; ${\text{P}}_{\text{L}} = $ class of schemes allowing labels as values; ${\text{P}}_{\text{M}} = $ class of schemes allowing a finite number of special markers as values; ${\text{P}}_{{\text{pds}}} = $ class of schemes using pushdown stores. With these, we can also discuss, for example, ${\text{P}}_{{\text{AM}}} $, the class of schemes allowing arrays, and special markers as values ; and ${\text{P}}_{{\text{AL}}} $, the class of schemes allowing arrays, and labels as values. We argue that ${\text{P}}_{\text{A}}$, ${\text{P}}_{\text{R}}$, and ${\text{P}}_{\text{L}}$ faithfully represent mechanisms of subscripting, recursion, and labels as values, that are present in many “real” programming languages. We show that \[ {\text{P}} < {\text{P}}_{\text{R}} < {\text{P}}_{\text{A}} \equiv {\text{P}}_{{\text{AM}}} \equiv {\text{P}}_{{\text{pdsM}}} \equiv {\text{P}}_{{\text{Ae}}} \equiv {\text{EF}}, \] where EF is Strong’s class of effective functionals, assuming total functions and predicates. The inclusions ${\text{P}} < {\text{P}}_{\text{R}} < {\text{P}}_{\text{A}} $ and equivalences ${\text{P}}_{{\text{AL}}} \equiv {\text{P}}_{{\text{AM}}} \equiv {\text{P}}_{{\text{pdsM}}} \equiv {\text{P}}_{{\text{Ae}}} $ are effective. For example, given a program scheme in ${\text{P}}_{{\text{AM}}} $ we can construct an equivalent one in ${\text{P}}_{{\text{AL}}} $. However, we show that for any scheme in ${\text{P}}_{{\text{AM}}} $ an equivalent ${\text{P}}_{\text{A}} $ scheme exists, but also prove it cannot (in general) be constructed! We conjecture that ${\text{P}}_{{\text{A}}} $, ${\text{P}}_{{\text{AL}}} $, and equivalent classes are indeed “universal.” The above results assume that the uninterpreted functions and predicates are total. We discuss the problems which arise when they are partial. We define the class of multischemes and outline the relationship between the class ${\text{P}}_{{\text{Ae}}} $, multischemes, and Strong’s nondeterministic and deterministic effective functionals.

We define a class of program schemata arising from the subrecursive programming language Loop. In this preliminary report on Loop schemata we show how to assign functional expressions to these schemata (as one aspect of the problem of assigning meaning to these programs), and we outline a solution to the schemata equivalence problem. Schemata equivalence is reduced to questions about formal expressions. Certain subcases of the problem are easily shown solvable, and although we claim that the general problem is solvable, we do not present the complete solution here because of its complexity.

The purpose of this paper is to give a model for the study of quantitative problems about formal translations from one programming language into another, as well as derive some initial results about the speed of programs produced by translations. The paper also contains a new speed-up result which shows that in any computational complexity measure there exist functions which have arbitrarily large speed-ups but that the size of the speed-up programs must grow non-computably fast.

This paper gives an overview of subrecursive hierarchy theory as it relates to computational complexity and applies some of the concepts to questions about the size of programs in subrecursive programming languages. The purpose is three-fold, to reveal in simple terms the workings of subrecursive hierarchies, to indicate new results in the area, and to point out ways that the fundamental ideas in hierarchy theory can lead to interesting questions about programming languages. A specific application yields new information about Blum's results on the size of programs and about the relationship between size and efficiency.