Robert L. Constable
#53,251
Most Influential Person Now
American computer scientist
Robert L. Constable's AcademicInfluence.com Rankings
Robert L. Constablecomputer-science Degrees
Computer Science
#2593
World Rank
#2712
Historical Rank
#1121
USA Rank
Robert L. Constablemathematics Degrees
Mathematics
#6035
World Rank
#8424
Historical Rank
#1883
USA Rank
Measure Theory
#2559
World Rank
#3068
Historical Rank
#728
USA Rank
Download Badge
Computer Science Mathematics
Why Is Robert L. Constable Influential?
(Suggest an Edit or Addition)According to Wikipedia, Robert Lee Constable is an American computer scientist. He is a professor of computer science and first and former dean of the Faculty of Computing and Information Science at Cornell University. He is known for his work on connecting computer programs and mathematical proofss, especially the Nuprl system. Prior to Nuprl, he worked on the PL/CV formal system and verifier. Alonzo Church was supervising the junior thesis of Robert while he was studying in Princeton. Constable received his PhD in 1968 under Stephen Kleene and has supervised over 40 students, including Edmund M. Clarke, Robert Harper, Kurt Mehlhorn, Steven Muchnick, Pavel Naumov, and Ryan Stansifer. He is a Fellow of the Association for Computing Machinery.
Robert L. Constable's Published Works
Number of citations in a given year to any of this author's works
Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author
Published Works
- Implementing mathematics with the Nuprl proof development system (1986) (1435)
- Infinite Objects in Type Theory (1986) (157)
- Proofs as programs (1985) (132)
- Building reliable, high-performance communication systems from components (2000) (123)
- Innovations in computational type theory using Nuprl (2006) (120)
- The semantics of reflected proof (1990) (111)
- Partial Objects In Constructive Type Theory (1987) (86)
- Constructive Mathematics and Automatic Program Writers (1970) (78)
- Logic for computer scientists (1989) (76)
- On Classes of Program Schemata (1971) (74)
- The Nuprl Open Logical Environment (2000) (72)
- Basic Statistics: Tales of Distributions. (1982) (68)
- Metalogical frameworks (1993) (67)
- MetaPRL - A Modular Logical Environment (2003) (66)
- Computability concepts for programming language semantics (1975) (57)
- Type two computational complexity (1973) (55)
- Formalized Metareasoning in Type Theory (1986) (54)
- Constructive Mathematics as a Programming Logic I: Some Principles of Theory (1983) (54)
- Computational foundations of basic recursive function theory (1988) (52)
- Protocol switching: exploiting meta-properties (2001) (50)
- The Type Theory of PL/CV3 (1984) (49)
- Verbalization of High-Level Formal Proofs (1999) (49)
- Recursive Definitions in Type Theory (1985) (46)
- Building reliable, high-performance communication systems from components (1999) (46)
- Developing Correctly Replicated Databases Using Formal Tools (2014) (44)
- Chapter X - Types in Logic, Mathematics and Programming (1998) (42)
- The Operator Gap (1969) (42)
- On the theory of programming logics (1977) (42)
- An Introduction to the PL/CV2 Programming Logic (1982) (40)
- On the Computational Complexity of Scheme Equivalence (1974) (39)
- A Logic of Events (2003) (37)
- Mathematics as Programming (1983) (36)
- Subrecursive Programming Languages, Part I: efficiency and program structure (1972) (36)
- Constructively formalizing automata theory (2000) (35)
- Finding computational content in classical proofs (1991) (33)
- Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML (2015) (31)
- Implementing Metamathematics as an Approach to Automatic Theorem Proving (1989) (29)
- Nuprl ’ s Class Theory and its Applications (2000) (26)
- The Logic of Events, a framework to reason about distributed systems (2012) (24)
- Naïve Computational Type Theory (2002) (23)
- Using Reflection to Explain and Enhance Type Theory (1995) (23)
- An experiment in formal design using meta-properties (2001) (23)
- FDL: A Prototype Formal Digital Library (2004) (23)
- Programs as Proofs: A Synopsis (1983) (22)
- The Structure of Nuprl’s Type Theory (1997) (21)
- Intuitionistic completeness of first-order logic (2011) (21)
- Dense and Non-Dense Families of Complexity Classes (1969) (20)
- Experience using type theory as a foundation for computer science (1991) (18)
- Nuprl as a General Logic (1989) (18)
- Knowledge-Based Synthesis of Distributed Systems Using Event Structures (2009) (18)
- The Semantics of Evidence (1985) (18)
- Formal Foundations of Computer Security (2008) (17)
- On the Computational Complexity of Program Scheme Equivalence (1980) (17)
- Computability Beyond Church-Turing via Choice Sequences (2018) (16)
- Logical Methods: In Honor of Anil Nerode's Sixtieth Birthday (1994) (16)
- Programs and types (1980) (15)
- Generating event logics with higher-order processes as realizers (2011) (15)
- A Type Theory with Partial Equivalence Relations as Types (2014) (15)
- Intensional analysis of functions and types (1982) (14)
- On the Efficiency of Programs in Subrecursive Formalisms (Incomplete Version, Extended Abstract) (1970) (14)
- A Causal Logic of Events in Formalized Computational Type Theory (2005) (14)
- Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics (2006) (13)
- Partial functions in constructive formal theories (1983) (13)
- ShadowDB: A Replicated Database on a Synthesized Consensus Core (2012) (13)
- On the size of programs in subrecursive formalisms (1970) (12)
- Logic and Program Semantics (2012) (11)
- The Nearly Ultimate Pearl (1983) (11)
- Assigning Meaning to Proofs: a semantic basis for problem solving environments (1989) (11)
- A diversified and correct-by-construction broadcast service (2012) (11)
- Programs as Proofs (1982) (10)
- Writing programs that construct proofs (2004) (10)
- Investigating correct-by-construction attack-tolerant systems (2011) (10)
- EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems (2017) (9)
- Logic and Program Semantics: essays dedicated to Dexter Kozen on the occasion of his 60th birthday (2012) (9)
- The Type Theory of PL/CV 3 (1981) (9)
- Bar induction: The good, the bad, and the ugly (2017) (9)
- Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP (2008) (9)
- Creating and evaluating interactive formal courseware for mathematics and computing (1996) (8)
- A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics. (2003) (8)
- A programming logic: With an introduction to the PL/CV verifier (1978) (7)
- Upward and Downward Diagonalization over Axiomatic Complexity Classes (1969) (7)
- PL/CS - A Disciplined Subset of PL/I (1976) (7)
- The Role of Finite Automata in the Development of Modern Computing Theory (1980) (7)
- Complexity of formal translations and speed-up results (1971) (7)
- Bar Induction is Compatible with Constructive Type Theory (2019) (6)
- Metalogical Frameworks II: Developing a Reflected Decision Procedure (1999) (6)
- Extracting the resolution algorithm from a completeness proof for the propositional calculus (2007) (6)
- Subrecursive Programming Languages. II. On Program Size (1971) (6)
- Computational type theory (2009) (6)
- A Constructive Programming Logic (1977) (6)
- A Graph-Based Approach Towards Discerning Inherent Structures in a Digital Library of Formal Mathematics (2004) (6)
- Recent Results in Type Theory and Their Relationship to Automath (2003) (6)
- A Constructive Theory of Recursive Functions (1973) (6)
- Review: Sheila A. Greibach, Theory of Program Structures: Schemes, Semantics, Verification (1978) (6)
- A Note on Complexity Measures for Inductive Classes in Constructive Type Theory (1998) (6)
- Implementing Euclid’s straightedge and compass constructions in type theory (2018) (5)
- A PL/CV precis (1979) (5)
- Representing Program Schemes in Logic (1972) (5)
- Reflecting the Open-Ended Computation System of Constructive Type Theory (1991) (5)
- Metalevel Programming in Constructive Type Theory (1992) (4)
- Transforming the Academy: Knowledge Formation in the Age of Digital Information (2005) (4)
- Automated computational complexity analysis (2001) (4)
- Expressing Computational Complexity in Constructive Type Theory (1994) (4)
- Formalizing Reference Types in NuPRL (1998) (4)
- Future Internet Enterprise Systems (2012) (4)
- Report on the Type Theory (V3) of the Programming Logic PL/CV3 (1980) (4)
- Subrecursive Program Schemata I & II: I. Undecidable Equivalence problems; II. Decidable Equivalence Problems (1972) (4)
- A Hierarchical Approach to Formal Semantics With Application to the Definition of PL/ CS (1979) (3)
- Introduction to EventML (2012) (3)
- On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer (2012) (3)
- Loop schemata (1971) (3)
- Computational complexity and induction for partial computable functions in type theory (2016) (3)
- Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle (2021) (3)
- Single change neighbor designs (1995) (2)
- Intuitionistic ancestral logic (2019) (2)
- Formal Systems, Logics, and Programs (2017) (2)
- An Elementary Formal Semantics for the Programming Language PL/CS (1976) (2)
- Brouwer’s Fan Theorem: An Overview (2016) (2)
- THEMES IN THE (1988) (2)
- Computability on Continuous Higher Types and its Role in the Semantics of Programming Languages (1974) (2)
- Formal Theories and Software Systems: Fundamental Connections between Computer Science and Logic (1992) (2)
- Virtual Evidence: A Constructive Semantics for Classical Logics (2014) (2)
- Enabling Large Scale Coherency Among Mathematical Texts (2006) (2)
- Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts (2006) (2)
- Mandates for a Changing Practice: PSRO and P.L. 94-142 (1980) (1)
- Evidence Semantics and Refinement Rules for First-Order Logics : Minimal , Intuitionistic , and Classical (2011) (1)
- Logical Aspects of Digital Mathematics Libraries ( extended abstract ) (2001) (1)
- Universally Closed Classes of Total Computable Functions (1984) (1)
- Nature of the Information Sciences (2000) (1)
- Lectures on:Classical Proofs as Programs (1993) (1)
- Proof, Language, and Interaction 2000 (2000) (1)
- The Triumph of Types: Principia Mathematica's Impact on Computer Science (2011) (1)
- Advanced Programming Languages CS6110 Spring 2012 Lecture 1 (2012) (1)
- Building Interactive Digital Libraries of Formal Algorithmic Knowledge (2003) (1)
- Formalizing Decidability Theorems About Automata (1999) (1)
- Nuprl ’ s Inductive Logical Forms (2015) (1)
- Notes on the “What is Information?” Workshop (2002) (1)
- Proceedings of the 15 th International Workshop on Automated Verification of Critical Systems ( AVoCS 2015 ) Formal Specification , Verification , and Implementation of Fault-Tolerant Systems (2015) (1)
- Language Features that Support Program Verification (illustrated in PL/C) (1976) (1)
- University of Birmingham Computability beyond Church-Turing via choice sequences (2018) (1)
- Information-intensive Proof Technology Contents 1 Series Introduction and Basics 4 (2003) (1)
- Subrecursive program schemata I & II(I. Undecidable equivalence problems, II. Decidable equivalence problems) (1972) (1)
- Themes in the development of programming logics circa 1963–1987 (1988) (1)
- The Triumph of Types : Creating a Logic of Computational Reality (2011) (1)
- Combinatorics: Positions in Room squares (1974) (1)
- Steps Toward a World Wide Digital Library of Formal Algorithmic Knowledge 1 (2003) (1)
- On the final coalgebra of automatic sequences. (2012) (0)
- A Conversation with Robert L. Constable (2015) (0)
- A Story of Bar Indu tion in (2016) (0)
- CS3110 Fall 2013 Lecture 1: Introduction, OCaml syntax, Evaluation (8/29) (2013) (0)
- Towards Integrated Systems for Symbolic Algebra and Formal Constructive Mathematics (1998) (0)
- The Definition of $\mu$PRL (1982) (0)
- AFRL-IF-WP-TM-2003 - (2003) (0)
- Max-planck-institut F Ur Informatik Metalogical Frameworks K I N F O R M a T I K Im Stadtwald D 66123 Saarbr Ucken Germany Authors' Addresses Publication Notes (2007) (0)
- The Fundamental Theorem of Arithmetic in PL/CV2 (1980) (0)
- Reflecting the computation system of constructive type theory in itself ∗ (2004) (0)
- Implementing Euclid’s straightedge and compass constructions in type theory (2018) (0)
- Discussing two topics : Synthetic Geometry and Atlantic Article (2017) (0)
- CS 6180 Lecture 25 – Event Logic , Computer Security , and Unguessable Atoms (2017) (0)
- Lecture 19 : Constructive Reals and Infinitesimal Calculus (2017) (0)
- CS 6180 Lecture 26 – Automated Reasoning and Ultra-Intuitionism (2017) (0)
- Greibach Sheila A.. Theory of program structures: schemes, semantics, verification. Lecture notes in computer science, vol. 36. Springer-Verlag, Berlin, Heidelberg, and New York, 1975, xv + 364 pp. (1978) (0)
- Subrecursive Programming Language III, The Multiple Recursive Functions, $\Re^{n}$ (1971) (0)
- RECENTRESULTS IN TYPE THEORY ANDTHEIR RELATIONSHIP TOAUTOMATH (2011) (0)
- Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations (2004) (0)
- ML Programming in Constructive Type Theory (abstract) (1997) (0)
- Russell's Orders in Kripke's Theory of Truth and Computational Type Theory (2012) (0)
- Two Lectures on Constructive Type Theory (2015) (0)
- Rules for program statements (1982) (0)
- A Conversation with Dexter Kozen (2015) (0)
- The Constructive Real Numbers (2017) (0)
- Applied Logic-CS 4860 (2016) (0)
- CS 6180 Lecture 22 – Theory of Computability in CTT (2017) (0)
- Subrecursive Programming Languages for $\Re^{n}$ (1970) (0)
- Max-planck-institut F ¨ Ur Informatik Metalogical Frameworks I N F O R M a T I K Authors' Addresses Publication Notes (2013) (0)
- CS 4860-2019 fa Computational Foundations of Mathematics (2019) (0)
- An Open Logical Programming Environment. A Practical Framework for Sharing Formal Models (2002) (0)
- Investigations of Type Theory in Programming Logics and Intelligent Systems (1985) (0)
- On the Relation of Refinement Between Algorithms (1973) (0)
- Bullying, and sexual harassment in schools: Pathways to assessment [Book Chapter] (2008) (0)
- Special SIGACT issue (1973) (0)
- CS4860-2020-Full-Lecture 6: PC and iPC are decidable (2020) (0)
- Formalizing Automata (2003) (0)
- CS 3110 Spring 2017 Lecture 25 : Course Review and Final Exam Coverage (2017) (0)
- Special issue on semantics and program schemas SIAM journal on computing (1974) (0)
- CS3110 Fall 2013 Lecture 6: Proving Properties of List Algorithms, Binary Search Trees (9/17) (2013) (0)
- Reflection and Propositions-as-Types (2007) (0)
- Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language (2015) (0)
- CS4860-Applied Logic 2020 Course Introduction (2020) (0)
- Applied Logic-CS 4860-2018-Lecture 2 (2018) (0)
- CS 3110 Spring 2017 Lecture 22 : Distributed Computing with Functional Processes continued (2016) (0)
- Computational Complexity and Brouwer’s Continuum (2020) (0)
- Lecture 24 – Constructive Type Theory (2016) (0)
- CS3110 Fall 2013 Lecture 2: Evaluation of Expressions, Types, Recursion (9/3) (2013) (0)
- Intuitionistic Completeness of First-Order Logic – mPC Case (2015) (0)
- Correct-by-Construction Attack-Tolerant Systems (2015) (0)
- Seminal Research Articles in Programming Languages (2015) (0)
- PX: A computational logic : S. Hayashi and N. Nakano, (MIT Press, London, 1988), price £24.75 (hardback), ISBN 0-262-08174-1 (1991) (0)
- A Computation Infrastructure for Knowledge-Based Development of Reliable Software Systems (2006) (0)
- CS / Math-4860 Course Description for Fall 2018 (2018) (0)
- Programs As Types (1980) (0)
- CS 6180 Lecture 24 – Asynchronous Distributed Computing (2017) (0)
- A Conversation with Claire Cardie (2015) (0)
- Active Models in Support of Collaborative Design (2001) (0)
- ADAPTIVE PROBABILISTIC PROTOCOLS FOR ADVANCED NETWORKS / ASSURING THE INTEGRITY OF HIGHLY DECENTRALIZED COMMUNICATIONS SYSTEMS (2005) (0)
- 2002 European Summer Meeting of the Association for Symbolic Logic Logic Colloquium '02 (2003) (0)
- Formally Generating Adaptive Security Protocols (2013) (0)
- Proof Assistants and the Dynamic Nature of Formal Theories (2012) (0)
- Building Mathematics-Based Software Systems to Advance Science and Create Knowledge (2009) (0)
- The Story of Logic – CS/Math 4860 Class Notes Fall 2019 (2011) (0)
- Book received (1956) (0)
- BioTT: a Family of Brouwerian Intuitionistic Theories Open to Classical Reasoning (2022) (0)
- Book reviews (2000) (0)
- Using Web Access to Formal Mathematics to Support Instruction in Computational Discrete Mathematics (2002) (0)
- CS3110 Spring 2017 Lecture 15: Constructive Synthetic Geometry (2017) (0)
- A Conversation with David Gries (2015) (0)
- VERking in constructive set theory (1981) (0)
- Applied Logic-CS 4860-2018 fa-Lecture 16 and 17 (2018) (0)
- Exporting and Refecting Abstract Metamathematics (1994) (0)
- Lecture 18 : The Constructive Real Numbers Continued (2017) (0)
- CS 3110 Spring 2016 Lecture 1 : Introduction , Course Plan , Elements of OCaml : Syntax , Evaluation ( 1 / 28 ) (2016) (0)
- Subrecursive Program Schemata I and III. Undecidable Equivalence Problems and II. Decidable EquivalenceProblems (1972) (0)
This paper list is powered by the following services:
Other Resources About Robert L. Constable
What Schools Are Affiliated With Robert L. Constable?
Robert L. Constable is affiliated with the following schools:
