Results for 'Curry-Howard correspondence'

1000+ found
Order:
  1.  56
    The placeholder view of assumptions and the CurryHoward correspondence.Ivo Pezlar - 2020 - Synthese (11):1-17.
    Proofs from assumptions are amongst the most fundamental reasoning techniques. Yet the precise nature of assumptions is still an open topic. One of the most prominent conceptions is the placeholder view of assumptions generally associated with natural deduction for intuitionistic propositional logic. It views assumptions essentially as holes in proofs, either to be filled with closed proofs of the corresponding propositions via substitution or withdrawn as a side effect of some rule, thus in effect making them an auxiliary notion subservient (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  2.  10
    Lectures on the Curry-Howard isomorphism.Morten Heine Sørensen - 2007 - Boston: Elsevier. Edited by Paweł Urzyczyn.
    The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance, minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc. The isomorphism has many aspects, even at the syntactic level: formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, proof (...)
    Direct download  
     
    Export citation  
     
    Bookmark   30 citations  
  3.  18
    CurryHoward–Lambek Correspondence for Intuitionistic Belief.Cosimo Perini Brogi - 2021 - Studia Logica 109 (6):1441-1461.
    This paper introduces a natural deduction calculus for intuitionistic logic of belief \ which is easily turned into a modal \-calculus giving a computational semantics for deductions in \. By using that interpretation, it is also proved that \ has good proof-theoretic properties. The correspondence between deductions and typed terms is then extended to a categorical semantics for identity of proofs in \ showing the general structure of such a modality for belief in an intuitionistic framework.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  4. The Significance of the Curry-Howard Isomorphism.Richard Zach - 2019 - In Gabriele Mras, Paul Weingartner & Bernhard Ritter (eds.), Philosophy of Logic and Mathematics: Proceedings of the 41st International Ludwig Wittgenstein Symposium. Berlin, Boston: De Gruyter. pp. 313-326.
    The Curry-Howard isomorphism is a proof-theoretic result that establishes a connection between derivations in natural deduction and terms in typed lambda calculus. It is an important proof-theoretic result, but also underlies the development of type systems for programming languages. This fact suggests a potential importance of the result for a philosophy of code.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  5.  9
    Derivation and Computation. Taking the Curry-Howard Correspondence Seriously.Norman Danner - 2001 - Bulletin of Symbolic Logic 7 (3):380-383.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  6.  4
    Derivation and computation: taking the Curry-Howard correspondence seriously.Harold Simmons - 2000 - New York: Cambridge University Press.
    Mathematics is about proofs, that is the derivation of correct statements; and calculations, that is the production of results according to well-defined sets of rules. The two notions are intimately related. Proofs can involve calculations, and the algorithm underlying a calculation should be proved correct. The aim of the author is to explore this relationship. The book itself forms an introduction to simple type theory. Starting from the familiar propositional calculus the author develops the central idea of an applied lambda-calculus. (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  7.  6
    Extended CurryHoward terms for second‐order logic.Pimpen Vejjajiva - 2013 - Mathematical Logic Quarterly 59 (4-5):274-285.
    In order to allow the use of axioms in a second‐order system of extracting programs from proofs, we define constant terms, a form of CurryHoward terms, whose types are intended to correspond to those axioms. We also define new reduction rules for these new terms so that all consequences of the axioms can be represented. We finally show that the extended CurryHoward terms are strongly normalizable.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  8.  26
    Simmons Harold. Derivation and computation. Taking the Curry-Howard correspondence seriously. Cambridge tracts in theoretical computer science, vol. 51. Cambridge University Press, Cambridge, New York, etc., 2000, xxv + 384 pp. [REVIEW]Norman Danner - 2001 - Bulletin of Symbolic Logic 7 (3):380-383.
  9. Are Uniqueness and Deducibility of Identicals the Same?Alberto Naibo & Mattia Petrolo - 2014 - Theoria 81 (2):143-181.
    A comparison is given between two conditions used to define logical constants: Belnap's uniqueness and Hacking's deducibility of identicals. It is shown that, in spite of some surface similarities, there is a deep difference between them. On the one hand, deducibility of identicals turns out to be a weaker and less demanding condition than uniqueness. On the other hand, deducibility of identicals is shown to be more faithful to the inferentialist perspective, permitting definition of genuinely proof-theoretical concepts. This kind of (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  10. Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations.Sara Ayhan - forthcoming - Journal of Logic and Computation.
    In this paper I will develop a lambda-term calculus, lambda-2Int, for a bi-intuitionistic logic and discuss its implications for the notions of sense and denotation of derivations in a bilateralist setting. Thus, I will use the Curry-Howard correspondence, which has been well-established between the simply typed lambda-calculus and natural deduction systems for intuitionistic logic, and apply it to a bilateralist proof system displaying two derivability relations, one for proving and one for refuting. The basis will be the (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  11.  14
    Under Lock and Key: A Proof System for a Multimodal Logic.G. A. Kavvos & Daniel Gratzer - 2023 - Bulletin of Symbolic Logic 29 (2):264-293.
    We present a proof system for a multimode and multimodal logic, which is based on our previous work on modal Martin-Löf type theory. The specification of modes, modalities, and implications between them is given as a mode theory, i.e., a small 2-category. The logic is extended to a lambda calculus, establishing a CurryHoward correspondence.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  12. Symmetric Categorial Grammar.Michael Moortgat - 2009 - Journal of Philosophical Logic 38 (6):681-710.
    The Lambek-Grishin calculus is a symmetric version of categorial grammar obtained by augmenting the standard inventory of type-forming operations (product and residual left and right division) with a dual family: coproduct, left and right difference. Interaction between these two families is provided by distributivity laws. These distributivity laws have pleasant invariance properties: stability of interpretations for the Curry-Howard derivational semantics, and structure-preservation at the syntactic end. The move to symmetry thus offers novel ways of reconciling the demands of (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  13.  8
    Typed lambda-calculus in classical Zermelo-Frænkel set theory.Jean-Louis Krivine - 2001 - Archive for Mathematical Logic 40 (3):189-205.
    , which uses the intuitionistic propositional calculus, with the only connective →. It is very important, because the well known Curry-Howard correspondence between proofs and programs was originally discovered with it, and because it enjoys the normalization property: every typed term is strongly normalizable. It was extended to second order intuitionistic logic, in 1970, by J.-Y. Girard [4], under the name of system F, still with the normalization property.More recently, in 1990, the Curry-Howard correspondence (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  14.  7
    From Proof-Objects to Grounds.Enrico Moriconi - 2024 - In Antonio Piccolomini D'Aragona (ed.), Perspectives on Deduction: Contemporary Studies in the Philosophy, History and Formal Theories of Deduction. Springer Verlag. pp. 115-138.
    The paper is devoted to an examination of the epistemic account of the notion of deductive inference recently provided by D. Prawitz, and based on the notion of ground. This is part of the general scenario constituted by the “Proof-theoretic semantics”, presented since the ’70s of the last century as an alternative to the standard model-theoretic explication of the notion of logical consequence.Our argument pivots on the so-called “CurryHoward Correspondence”, which exploited the idea of considering proofs as (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  15.  8
    Lambek–Grishin Calculus: Focusing, Display and Full Polarization.Giuseppe Greco, Michael Moortgat, Valentin D. Richard & Apostolos Tzimoulis - 2023 - In Alessandra Palmigiano & Mehrnoosh Sadrzadeh (eds.), Samson Abramsky on Logic and Structure in Computer Science and Beyond. Springer Verlag. pp. 877-915.
    Focused sequent calculi are a refinement of sequent calculi, where additional side-conditions on the applicability of inference rules force the implementation of a proof search strategy. Focused cut-free proofs exhibit a special normal form that is used for defining identity of sequent calculi proofs. We introduce a novel focused display calculus fD.LG and a fully polarized algebraic semantics FP.LG\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbb {FP.LG}$$\end{document} for Lambek–Grishin logic by generalizing the theory of multi-type calculi and their (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  16.  82
    Lambda Grammars and the Syntax-Semantics Interface.Reinhard Muskens - 2001 - In Robert Van Rooij & Martin Stokhof (eds.), Proceedings of the Thirteenth Amsterdam Colloquium. Amsterdam: ILLC. pp. 150-155.
    In this paper we discuss a new perspective on the syntax-semantics interface. Semantics, in this new set-up, is not ‘read off’ from Logical Forms as in mainstream approaches to generative grammar. Nor is it assigned to syntactic proofs using a Curry-Howard correspondence as in versions of the Lambek Calculus, or read off from f-structures using Linear Logic as in Lexical-Functional Grammar (LFG, Kaplan & Bresnan [9]). All such approaches are based on the idea that syntactic objects (trees, (...)
    Direct download  
     
    Export citation  
     
    Bookmark   8 citations  
  17.  56
    A resource sensitive interpretation of lexical functional grammar.Mark Johnson - 1999 - Journal of Logic, Language and Information 8 (1):45-81.
    This paper investigates whether the fundamental linguistic insights and intuitions of Lexical Functional Grammar, which is usually presented as a constraint-based linguistic theory, can be reformulated in a resource sensitive framework using a substructural modal logic. In the approach investigated here, LFG's f-descriptions are replaced with expressions from a multi-modal propositional logic. In effect, the feature structure unification basis of LFG's f-structures is replaced with a very different resource based mechanism. It turns out that some linguistic analyses that required non-monotonic (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark  
  18.  15
    Les intuitions logiques d’Edgar Morin.Didier Dacunha-Castelle - 2011 - Hermès: La Revue Cognition, communication, politique 60 (2):, [ p.].
    Les mathématiques telles qu’elles se sont développées entre 1935 et 1970 jouent un rôle très important dans La Méthode. Ce rôle est explicite en ce qui concerne la logique, plus implicite en ce qui concerne la théorie du contrôle, l’incertitude, et certaines notions vues hors du champ mathématique et particulièrement probabiliste . Sur un exemple de résultats récents de la logique mathématique, la correspondance de Curry-Howard et les travaux de Jean-Louis Krivine nous montrent la pertinence des idées et (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  19. Imperative programs as proofs via game semantics.Martin Churchill, Jim Laird & Guy McCusker - 2013 - Annals of Pure and Applied Logic 164 (11):1038-1078.
    Game semantics extends the CurryHoward isomorphism to a three-way correspondence: proofs, programs, strategies. But the universe of strategies goes beyond intuitionistic logics and lambda calculus, to capture stateful programs. In this paper we describe a logical counterpart to this extension, in which proofs denote such strategies. The system is expressive: it contains all of the connectives of Intuitionistic Linear Logic, and first-order quantification. Use of Lairdʼs sequoid operator allows proofs with imperative behaviour to be expressed. Thus, we (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  20.  48
    Ternary relations and relevant semantics.Robert K. Meyer - 2004 - Annals of Pure and Applied Logic 127 (1-3):195-217.
    Modus ponens provides the central theme. There are laws, of the form A→C. A logic L collects such laws. Any datum A provides input to the laws of L. The central ternary relation R relates theories L,T and U, where U consists of all of the outputs C got by applying modus ponens to major premises from L and minor premises from T. Underlying this relation is a modus ponens product operation on theories L and T, whence RLTU iff LTU. (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  21.  15
    A lambda proof of the p-w theorem.Sachio Hirokawa, Yuichi Komori & Misao Nagayama - 2000 - Journal of Symbolic Logic 65 (4):1841-1849.
    The logical system P-W is an implicational non-commutative intuitionistic logic defined by axiom schemes B = (b → c) → (a → b) → a → c, B' = (a → b) → (b → c) → a → c, I = a → a with the rules of modus ponens and substitution. The P-W problem is a problem asking whether α = β holds if α → β and β → α are both provable in P-W. The answer is (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark  
  22.  3
    Lambda Calculus and Intuitionistic Linear Logic.Simona Della Rocca & Luca Roversi - 1997 - Studia Logica 59 (3):417-448.
    The introduction of Linear Logic extends the Curry-Howard Isomorphism to intensional aspects of the typed functional programming. In particular, every formula of Linear Logic tells whether the term it is a type for, can be either erased/duplicated or not, during a computation. So, Linear Logic can be seen as a model of a computational environment with an explicit control about the management of resources.This paper introduces a typed functional language Λ! and a categorical model for it.The terms of (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  23.  19
    On the unity of duality.Noam Zeilberger - 2008 - Annals of Pure and Applied Logic 153 (1-3):66-96.
    Most type systems are agnostic regarding the evaluation strategy for the underlying languages, with the value restriction for ML which is absent in Haskell as a notable exception. As type systems become more precise, however, detailed properties of the operational semantics may become visible because properties captured by the types may be sound under one strategy but not the other. For example, intersection types distinguish between call-by-name and call-by-value functions, because the subtyping law ∩≤A→ is unsound for the latter in (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  24.  7
    A Concrete Categorical Model for the Lambek Syntactic Calculus.Marcelo Da Silva Corrêa & Edward Hermann Haeusler - 1997 - Mathematical Logic Quarterly 43 (1):49-59.
    We present a categorical/denotational semantics for the Lambek Syntactic Calculus , indeed for a λlD-typed version Curry-Howard isomorphic to it. The main novelty of our approach is an abstract noncommutative construction with right and left adjoints, called sequential product. It is defined through a hierarchical structure of categories reflecting the implicit permission to sequence expressions and the inductive construction of compound expressions. We claim that Lambek's noncommutative product corresponds to a noncommutative bi-endofunctor into a category, which encloses all (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  25.  82
    Categorial grammar and discourse representation theory.Reinhard Muskens - 1994 - In Yorick Wilks (ed.), Proceedings of COLING 94. Kyoto: pp. 508-514.
    In this paper it is shown how simple texts that can be parsed in a Lambek Categorial Grammar can also automatically be provided with a semantics in the form of a Discourse Representation Structure in the sense of Kamp [1981]. The assignment of meanings to texts uses the Curry-Howard-Van Benthem correspondence.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  26.  19
    Une preuve formelle et intuitionniste du théorème de complétude de la logique classique.Jean-Louis Krivine - 1996 - Bulletin of Symbolic Logic 2 (4):405-421.
    Introduction. Il est bien connu que la correspondance de Curry-Howard permet d'associer un programme, sous la forme d'un λ-terme, à toute preuve intuitionniste, formalisée dans le calcul des prédicats du second ordre. Cette correspondance a été étendue, assez récemment, à la logique classique moyennant une extension convenable du λ-calcul. Chaque théorème formalisé en logique du second ordre correspond donc à une spécification de programme.Il se pose alors le problème, en général tout à fait non trivial, de trouver la (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  27.  7
    The Curry-Howard isomorphism.Philippe De Groote (ed.) - 1995 - Louvain-la-Neuve: Academia.
  28.  15
    A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
    The lambdaPi-calculus, a theory of first-order dependent function types in Curry-Howard-de Bruijn correspondence with a fragment of minimal first-order logic, is defined as a system of (linearized) natural deduction. In this paper, we present a Gentzen-style sequent calculus for the lambdaPi-calculus and prove the cut-elimination theorem. The cut-elimination result builds upon the existence of normal forms for the natural deduction system and can be considered to be analogous to a proof provided by Prawitz for first-order logic. The (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  29. On the correspondence between proofs and lamba-terms.J. Gallier - 1995 - In Philippe De Groote (ed.), The Curry-Howard isomorphism. Louvain-la-Neuve: Academia.
     
    Export citation  
     
    Bookmark   3 citations  
  30.  5
    Curry-Howard terms for linear logic.Frank A. Bäuerle, David Albrecht, John N. Crossley & John S. Jeavons - 1998 - Studia Logica 61 (2):223-235.
    In this paper we 1. provide a natural deduction system for full first-order linear logic, 2. introduce Curry-Howard-style terms for this version of linear logic, 3. extend the notion of substitution of Curry-Howard terms for term variables, 4. define the reduction rules for the Curry-Howard terms and 5. outline a proof of the strong normalization for the full system of linear logic using a development of Girard's candidates for reducibility, thereby providing an alternative to (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  31.  9
    Notes & Correspondence.Howard Gruber, Oystein Ore & A. Hall - 1961 - Isis 52:582-586.
  32.  12
    Notes & Correspondence.Howard E. Gruber, Oystein Ore, A. Rupert Hall, Marie Boas Hall & Waclaw Slabczynski - 1961 - Isis 52 (4):582-586.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  33.  10
    Extending the Curry-Howard interpretation to linear, relevant and other resource logics.Dov M. Gabbay & Ruy J. G. B. de Queiroz - 1992 - Journal of Symbolic Logic 57 (4):1319-1365.
  34. Truth About Artifacts.Howard Sankey - 2023 - Symposion: Theoretical and Applied Inquiries in Philosophy and Social Sciences 10 (1):149-152.
    Truth in a correspondence sense is objective in two ways. It is objective because the relation of correspondence is objective and because the facts to which truths correspond are objective. Truth about artifacts is problematic because artifacts are intentionally designed to perform certain functions, and so are not entirely mind independent. Against this, it is argued in this paper that truth about artifacts is perfectly objective despite the role played by intention and purpose in the production of artifacts.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  35. Extending the Curry {Howard {Tait interpretation to linear, relevant and other logics.D. M. Gabbay & Rjgb de Queiroz - 1992 - Journal of Symbolic Logic 56:1129-40.
  36.  10
    Extending the Curry-Howard Interpretation to Linear, Relevant and Other Resource Logics.Dov M. Gabbay & Ruy J. G. B. De Queiroz - 1992 - Journal of Symbolic Logic 57 (4):1319 - 1365.
  37.  76
    Can beliefs correspond to reality?Howard Darmstadter - 1974 - Journal of Philosophy 71 (10):302-314.
  38.  39
    Maximization theory and Plato's concept of the Good.Howard Rachlin - 1985 - Behaviorism 13 (1):3-20.
    Plato's dialogues may be interpreted in a number of ways. One interpretation sees Plato's concept of The Good as a precursor of maximization theory, a modern behavioral theory. Plato identifies goodness with an ideal pattern of people's overt choices under the constraints of everyday life. Correspondingly, maximization theory sees goodness (in terms of "value") as a quantifiable function of overt, constrained choices of an animal. In both conceptions goodness may be increased by expanding the temporal extent over which a behavioral (...)
    Direct download  
     
    Export citation  
     
    Bookmark   30 citations  
  39. Realism and Conventionalism in Einstein's Philosophy of Science: The Einstein-Schlick Correspondence.D. A. Howard - 1984 - Philosophia Naturalis 21 (2/4):616.
  40.  36
    Reduction Rules for Intuitionistic $${{\lambda}{\rho}}$$ λ ρ -calculus.Ken-Etsu Fujita, Ryo Kashima, Yuichi Komori & Naosuke Matsuda - 2015 - Studia Logica 103 (6):1225-1244.
    The third author gave a natural deduction style proof system called the \-calculus for implicational fragment of classical logic in. In -calculus, 2015, Post-proceedings of the RIMS Workshop “Proof Theory, Computability Theory and Related Issues”, to appear), the fourth author gave a natural subsystem “intuitionistic \-calculus” of the \-calculus, and showed the system corresponds to intuitionistic logic. The proof is given with tree sequent calculus, but is complicated. In this paper, we introduce some reduction rules for the \-calculus, and give (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  41.  30
    Further Considerations on Newton's Methods.Howard Stein - unknown
    Discussion at the symposium, and subsequent correspondence with participants, have raised a series of critical questions that seem to me to merit discussion. The issues raised have also led me to consider further some of the literature commenting on Newton’s work and on related matters in the history of optics. What was initially intended as a brief supplement to the foregoing paper [On Metaphysics and Method in Newton, item 10631] has thus evolved into a new article of considerable length.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  42.  23
    Oracles and Query Lower Bounds in Generalised Probabilistic Theories.Howard Barnum, Ciarán M. Lee & John H. Selby - 2018 - Foundations of Physics 48 (8):954-981.
    We investigate the connection between interference and computational power within the operationally defined framework of generalised probabilistic theories. To compare the computational abilities of different theories within this framework we show that any theory satisfying four natural physical principles possess a well-defined oracle model. Indeed, we prove a subroutine theorem for oracles in such theories which is a necessary condition for the oracle model to be well-defined. The four principles are: causality, purification, strong symmetry, and informationally consistent composition. Sorkin has (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  43.  5
    The Semantics of Entailment Omega.Yoko Motohama, Robert K. Meyer & Mariangiola Dezani-Ciancaglini - 2002 - Notre Dame Journal of Formal Logic 43 (3):129-145.
    This paper discusses the relation between the minimal positive relevant logic B and intersection and union type theories. There is a marvelous coincidence between these very differently motivated research areas. First, we show a perfect fit between the Intersection Type Discipline ITD and the tweaking BT of B, which saves implication and conjunction but drops disjunction . The filter models of the -calculus (and its intimate partner Combinatory Logic CL) of the first author and her coauthors then become theory models (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  44. An introduction to the Leibniz-Clarke correspondence.Howard Robert Bernstein - 1972 - [New York]: [New York].
  45. Basic theory of functionality. Analogies with propositional algebra.H. B. Curry & R. Feys - 1995 - In Philippe De Groote (ed.), The Curry-Howard isomorphism. Louvain-la-Neuve: Academia.
     
    Export citation  
     
    Bookmark   1 citation  
  46.  28
    How an Unsurpassable Being Can Create a Surpassable World.Daniel Howard-Snyder & Frances Howard-Snyder - 1994 - Faith and Philosophy 11 (2):260-268.
    Imagine that there exists a good, essentially omniscient and omnipotent being named Jove, and that there exists nothing else. No possible being is more powerful or knowledgable. Out of his goodness, Jove decides to create. Since he is all-powerful, there is nothing but the bounds of possibility to prevent him from getting what he wants. Unfortunately, as he holds before his mind the host of worlds, Jove sees that for each there is a better one. Although he can create any (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   27 citations  
  47. Both sides of the story: explaining events in a narrative.Gregory Currie - 2007 - Philosophical Studies 135 (1):49-63.
    Our experience of narrative has an internal and an external aspect--the content of the narrative’s representations, and its intentional, communicative aetiology. The interaction of these two things is crucial to understanding how narrative works. I begin by laying out what I think we can reasonably expect from a narrative by way of causal information, and how causality interacts with other attributes we think of as central to narrative. At a certain point this discussion will strike a problem: our judgements about (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  48. The formulæ-as-types notion of construction.W. A. Howard - 1995 - In Philippe De Groote (ed.), The Curry-Howard isomorphism. Louvain-la-Neuve: Academia.
     
    Export citation  
     
    Bookmark   68 citations  
  49. A Study To Evaluate The Effect Of Investigator Attendance On The Efficiency Of Irb Review.Holly Taylor, Peter Currie & Nancy Kass - 2008 - IRB: Ethics & Human Research 30 (1):1-5.
    We conducted a retrospective review of research protocols from four IRBs at one large academic medical institution. The project examined whether having the Principal Investigator attend the initial IRB review of his or her study improves the efficiency of the review. We measured efficiency by the number of days from protocol submission to approval, volume of correspondence exchanged between investigator and IRB prior to approval, and the number of convened IRB meetings required prior to approval. We assessed two samples (...)
     
    Export citation  
     
    Bookmark   1 citation  
  50.  31
    Consciousness, memory, and the hippocampal system: What kind of connections can we make?Howard Eichenbaum & Neal J. Cohen - 1995 - Behavioral and Brain Sciences 18 (4):680-681.
    Gray's account is remarkable in its depth and scope but too little attention is paid to poor correspondences with the literature on hippocampal/subicular damage, the theta rhythm, and novelty detection. An alternative account, focusing on hippocampal involvement in organizing memories in a way that makes them accessible to conscious recollection but not in access to consciousness per se, avoids each of these limitations.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
1 — 50 / 1000