Search

Your search keyword '"Constable, Robert L."' showing total 208 results
Start Over Author "Constable, Robert L."
208 results on '"Constable, Robert L."'

1. Virtual Evidence: A Constructive Semantics for Classical Logics

Author

Constable, Robert L.

Subjects
Computer Science - Logic in Computer Science
Abstract

This article presents a computational semantics for classical logic using constructive type theory. Such semantics seems impossible because classical logic allows the Law of Excluded Middle (LEM), not accepted in constructive logic since it does not have computational meaning. However, the apparently oracular powers expressed in the LEM, that for any proposition P either it or its negation, not P, is true can also be explained in terms of constructive evidence that does not refer to "oracles for truth." Types with virtual evidence and the constructive impossibility of negative evidence provide sufficient semantic grounds for classical truth and have a simple computational meaning. This idea is formalized using refinement types, a concept of constructive type theory used since 1984 and explained here. A new axiom creating virtual evidence fully retains the constructive meaning of the logical operators in classical contexts. Key Words: classical logic, constructive logic, intuitionistic logic, propositions-as-types, constructive type theory, refinement types, double negation translation, computational content, virtual evidence

Published
2014

4. Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language

Author

Cohen, Liron, Constable, Robert L., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, de Paiva, Valeria, editor, de Queiroz, Ruy, editor, Moss, Lawrence S., editor, Leivant, Daniel, editor, and de Oliveira, Anjolina G., editor

Published
2015
Full Text
View/download PDF

5. Building Mathematics-Based Software Systems to Advance Science and Create Knowledge

Author

Constable, Robert L., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Albers, Susanne, editor, Alt, Helmut, editor, and Näher, Stefan, editor

Published
2009
Full Text
View/download PDF

8. MetaPRL – A Modular Logical Environment

Author

Hickey, Jason, Nogin, Aleksey, Constable, Robert L., Aydemir, Brian E., Barzilay, Eli, Bryukhov, Yegor, Eaton, Richard, Granicz, Adam, Kopylov, Alexei, Kreitz, Christoph, Krupski, Vladimir N., Lorigo, Lori, Schmitt, Stephan, Witty, Carl, Yu, Xin, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, Basin, David, editor, and Wolff, Burkhart, editor

Published
2003
Full Text
View/download PDF

10. The Nuprl Open Logical Environment

Author

Allen, Stuart F., Constable, Robert L., Eaton, Rich, Kreitz, Christoph, Lorigo, Lori, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, and McAllester, David, editor

Published
2000
Full Text
View/download PDF

13. Bar Induction is Compatible with Constructive Type Theory.

Author

RAHLI, VINCENT, BICKFORD, MARK, COHEN, LIRON, and CONSTABLE, ROBERT L.

Subjects
PROGRAMMING languages, TYPE theory, INVARIANT theory
Abstract

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 FROM AUTHOR]

Published
2019
Full Text
View/download PDF

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

Author

Bickford, Mark, Cohen, Liron, Constable, Robert L., and Rahli, Vincent

Subjects
Realizability, Constructive Type Theory, Choice sequences, Classical Logic, Coq, Theory of computation → Type theory, Theory of computation → Constructive mathematics, Intuitionism, Theorem proving, Extensional type theory, Law of Excluded Middle
Abstract

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., LIPIcs, Vol. 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), pages 11:1-11:23

Published
2021
Full Text
View/download PDF

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

Author

Mark Bickford and Liron Cohen and Robert L. Constable and Vincent Rahli, Bickford, Mark, Cohen, Liron, Constable, Robert L., Rahli, Vincent, Mark Bickford and Liron Cohen and Robert L. Constable and Vincent Rahli, Bickford, Mark, Cohen, Liron, Constable, Robert L., and Rahli, Vincent

Abstract

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.

Published
2021
Full Text
View/download PDF

39. Partial functions in comstructive formal theories

Author

Constable, Robert L., Goos, G., editor, Hartmanis, J., editor, Barstow, D., editor, Brauer, W., editor, Brinch Hansen, P., editor, Gries, D., editor, Luckham, D., editor, Moler, C., editor, Pnueli, A., editor, Seegmüller, G., editor, Stoer, J., editor, Wirth, N., editor, Cremers, Armin B., editor, and Kriegel, Hans-Peter, editor

Published
1982
Full Text
View/download PDF

40. The type theory of PL/CV3

Author

Constable, Robert L., Zlatin, Daniel R., Goos, G., editor, Hartmanis, J., editor, Brauer, W., editor, Brinch Hansen, P., editor, Gries, D., editor, Moler, C., editor, Seegmüller, G., editor, Stoer, J., editor, Wirth, N., editor, and Kozen, Dexter, editor

Published
1982
Full Text
View/download PDF

44. Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML

Author

Rahli, Vincent, Guaspari, David, Bickford, Mark, and Constable, Robert L.

Subjects
Computer science [C05] [Engineering, computing & technology], Sciences informatiques [C05] [Ingénierie, informatique & technologie]
Abstract

Distributed programs are known to be extremely difficult to implement, test, verify, and maintain. This is due in part to the large number of possible unforeseen interactions among components, and to the difficulty of precisely specifying what the programs should accomplish in a formal language that is intuitively clear to the programmers. We discuss here a methodology that has proven itself in building a state of the art implementation of Multi-Paxos and other distributed protocols used in a deployed database system. This article focuses on the basic ideas of formal EventML programming illustrated by implementing a fault-tolerant consensus protocol and showing how we prove its safety properties with the Nuprl proof assistant., Electronic Communications of the EASST, Volume 72: Proceedings of the 15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015)

Published
2015
Full Text
View/download PDF

47. A Type Theory with Partial Equivalence Relations as Types

Author

Anand, Abhishek, Bickford, Mark, Constable, Robert L., and Rahli, Vincent

Subjects
Computer science [C05] [Engineering, computing & technology], Sciences informatiques [C05] [Ingénierie, informatique & technologie]
Published
2014

48. Introduction to EventML

Author

Bickford, Mark, Constable, Robert L., Eaton, Richard, Guaspari, David, and Rahli, Vincent

Subjects
Computer science [C05] [Engineering, computing & technology], Sciences informatiques [C05] [Ingénierie, informatique & technologie]
Published
2012

Catalog

Books, media, physical & digital resources
See catalog results