13 found
Robert L. Constable [7]R. L. Constable [3]Robert Constable [2]R. Todd Constable [2]
R. T. Constable [1]
  1.  21
    Characterizing Attention with Predictive Network Models.M. D. Rosenberg, E. S. Finn, D. Scheinost, R. T. Constable & M. M. Chun - 2017 - Trends in Cognitive Sciences 21 (4):290-302.
  2.  16
    Implementing Mathematics with the Nuprl Proof Development System.R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer & R. W. Harper - 1990 - Journal of Symbolic Logic 55 (3):1299-1302.
  3.  10
    Innovations in Computational Type Theory Using Nuprl.S. F. Allen, M. Bickford, R. L. Constable, R. Eaton, C. Kreitz, L. Lorigo & E. Moran - 2006 - Journal of Applied Logic 4 (4):428-469.
    Direct download (3 more)  
    Export citation  
    Bookmark   5 citations  
  4.  43
    Types in Logic, Mathematics and Programming.Robert L. Constable - 1998 - In Samuel R. Buss (ed.), Bulletin of Symbolic Logic. Elsevier. pp. 137.
  5.  11
    2002 European Summer Meeting of the Association for Symbolic Logic Logic Colloquium'02.Lev D. Beklemishev, Stephen Cook, Olivier Lessmann, Simon Thomas, Jeremy Avigad, Arnold Beckmann, Tim Carlson, Robert L. Constable & Kosta Došen - 2003 - Bulletin of Symbolic Logic 9 (1):71.
  6.  5
    Extracting the Resolution Algorithm From a Completeness Proof for the Propositional Calculus.Robert Constable & Wojciech Moczydłowski - 2010 - Annals of Pure and Applied Logic 161 (3):337-348.
    We prove constructively that for any propositional formula in Conjunctive Normal Form, we can either find a satisfying assignment of true and false to its variables, or a refutation of showing that it is unsatisfiable. This refutation is a resolution proof of ¬. From the formalization of our proof in Coq, we extract Robinson’s famous resolution algorithm as a Haskell program correct by construction. The account is an example of the genre of highly readable formalized mathematics.
    Direct download (6 more)  
    Export citation  
  7.  21
    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. [REVIEW]Robert L. Constable - 1978 - Journal of Symbolic Logic 43 (1):154-156.
  8.  24
    Intuitionistic Completeness of First-Order Logic.Robert Constable & Mark Bickford - 2014 - Annals of Pure and Applied Logic 165 (1):164-198.
    We constructively prove completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable in iFOL if and only if it is uniformly valid in intuitionistic evidence semantics as defined in intuitionistic type theory extended with an intersection operator.Our completeness proof provides an effective procedure that converts any uniform evidence into a formal iFOL proof. Uniform evidence can involve arbitrary concepts from type theory such as ordinals, topological structures, algebras and so forth. We have implemented that procedure in the (...)
    Direct download (7 more)  
    Export citation  
  9.  10
    Review: Sheila A. Greibach, Theory of Program Structures: Schemes, Semantics, Verification. [REVIEW]Robert L. Constable - 1978 - Journal of Symbolic Logic 43 (1):154-156.
  10. The Role of Finite Automata in the Development of Modern Computing Theory.Robert L. Constable - 1980 - In J. Barwise, H. J. Keisler & K. Kunen (eds.), The Kleene Symposium. North-Holland. pp. 61--83.
  11.  37
    The Triumph of Types: Principia Mathematica's Impact on Computer Science.Robert L. Constable - unknown
    Types now play an essential role in computer science; their ascent originates from Principia Mathematica. Type checking and type inference algorithms are used to prevent semantic errors in programs, and type theories are the native language of several major interactive theorem provers. Some of these trace key features back to Principia.
    Direct download  
    Export citation  
  12.  17
    Metonymy as Referential Dependency: Psycholinguistic and Neurolinguistic Arguments for a Unified Linguistic Treatment.Maria M. Piñango, Muye Zhang, Emily Foster‐Hanson, Michiro Negishi, Cheryl Lacadie & R. Todd Constable - 2017 - Cognitive Science 41 (S2).
    We examine metonymy at psycho- and neurolinguistic levels, seeking to adjudicate between two possible processing implementations. We compare highly conventionalized systematic metonymy to lesser-conventionalized circumstantial metonymy. Whereas these two metonymy types differ in terms of contextual demands, they each reveal a similar dependency between the named and intended conceptual entities. We reason that if each metonymy yields a distinct processing time course and substantially non-overlapping preferential localization pattern, it would not only support a two-mechanism view but would suggest that conventionalization (...)
    No categories
    Direct download (3 more)  
    Export citation  
  13.  10
    Insula as the Interface Between Body Awareness and Movement: A Neurofeedback-Guided Kinesthetic Motor Imagery Study in Parkinson’s Disease.Sule Tinaz, Kiran Para, Ana Vives-Rodriguez, Valeria Martinez-Kaigi, Keerthana Nalamada, Mine Sezgin, Dustin Scheinost, Michelle Hampson, Elan D. Louis & R. Todd Constable - 2018 - Frontiers in Human Neuroscience 12.