9 found
Order:
  1.  36
    James Ladyman & Stuart Presnell (2015). Identity in Homotopy Type Theory, Part I: The Justification of Path Induction. Philosophia Mathematica 23 (3):386-406.
    Homotopy Type Theory is a proposed new language and foundation for mathematics, combining algebraic topology with logic. An important rule for the treatment of identity in HoTT is path induction, which is commonly explained by appeal to the homotopy interpretation of the theory's types, tokens, and identities as spaces, points, and paths. However, if HoTT is to be an autonomous foundation then such an interpretation cannot play a fundamental role. In this paper we give a derivation of path induction, motivated (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  2.  71
    James Ladyman, Stuart Presnell, Anthony J. Short & Berry Groisman (2007). The Connection Between Logical and Thermodynamic Irreversibility. Studies in History and Philosophy of Science Part B 38 (1):58-79.
    There has recently been a good deal of controversy about Landauer's Principle, which is often stated as follows: The erasure of one bit of information in a computational device is necessarily accompanied by a generation of kTln2 heat. This is often generalised to the claim that any logically irreversible operation cannot be implemented in a thermodynamically reversible way. John Norton (2005) and Owen Maroney (2005) both argue that Landauer's Principle has not been shown to hold in general, and Maroney offers (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   5 citations  
  3.  17
    James Ladyman & Stuart Presnell, Does Homotopy Type Theory Provide a Foundation for Mathematics?
    Homotopy Type Theory is a putative new foundation for mathematics grounded in constructive intensional type theory, that offers an alternative to the foundations provided by ZFC set theory and category theory. This paper explains and motivates an account of how to define, justify and think about HoTT in a way that is self-contained, and argues that it can serve as an autonomous foundation for mathematics. We first consider various questions that a foundation for mathematics might be expected to answer, and (...)
    No categories
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  4.  16
    James Ladyman & Stuart Presnell, Identity in HoTT, Part I.
    Homotopy type theory is a new branch of mathematics that connects algebraic topology with logic and computer science, and which has been proposed as a new language and conceptual framework for math- ematical practice. Much of the power of HoTT lies in the correspondence between the formal type theory and ideas from homotopy theory, in par- ticular the interpretation of types, tokens, and equalities as spaces, points, and paths. Fundamental to the use of identity and equality in HoTT is the (...)
    No categories
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  5.  15
    James Ladyman & Stuart Presnell, A Primer on Homotopy Type Theory Part 1: The Formal Type Theory.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  6. James Ladyman, Stuart Presnell & Anthony J. Short (2008). The Use of the Information-Theoretic Entropy in Thermodynamics. Studies in History and Philosophy of Science Part B 39 (2):315-324.
    When considering controversial thermodynamic scenarios such as Maxwell's demon, it is often necessary to consider probabilistic mixtures of states. This raises the question of how, if at all, to assign entropy to them. The information-theoretic entropy is often used in such cases; however, no general proof of the soundness of doing so has been given, and indeed some arguments against doing so have been presented. We offer a general proof of the applicability of the information-theoretic entropy to probabilistic mixtures of (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  7.  53
    Tony Short, James Ladyman, Berry Groisman & Stuart Presnell, The Connection Between Logical and Thermodynamical Irreversibility.
    There has recently been a good deal of controversy about Landauer's Principle, which is often stated as follows: The erasure of one bit of information in a computational device is necessarily accompanied by a generation of kT ln 2 heat. This is often generalised to the claim that any logically irreversible operation cannot be implemented in a thermodynamically reversible way. John Norton (2005) and Owen Maroney (2005) both argue that Landauer's Principle has not been shown to hold in general, and (...)
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  8. James Ladyman, Stuart Presnell, Anthony J. Short & Berry Groisman (2007). The Connection Between Logical and Thermodynamic Irreversibility. Studies in History and Philosophy of Science Part B: Studies in History and Philosophy of Modern Physics 38 (1):58-79.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  9. James Ladyman, Stuart Presnell & Anthony J. Short (2008). The Use of the Information-Theoretic Entropy in Thermodynamics. Studies in History and Philosophy of Science Part B: Studies in History and Philosophy of Modern Physics 39 (2):315-324.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography