Jonkman Microblog
  • Login
Show Navigation
  • Public

    • Public
    • Network
    • Groups
    • Popular
    • People

Conversation

Notices

  1. Fabián Heredia 🚲 (fabianhjr@social.coop)'s status on Tuesday, 05-Dec-2017 01:26:01 EST Fabián Heredia 🚲 Fabián Heredia 🚲

    @natecull @akkartik @seanl

    The Curry-Howard correspondence is between Simpled Typed Lambda Calculus and Propositional Intuisionistic Logic.

    Per Martin-Löf added dependent types, types that can depend on the value of their arguments, to create Intuisionistic Type Theory which corresponds to Intuisionistic Predicate Calculus.

    So with that bigger TT, you can prove stuff on computers like:

    https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Nat.idr#L480

    In conversation Tuesday, 05-Dec-2017 01:26:01 EST from social.coop permalink
  • Help
  • About
  • FAQ
  • TOS
  • Privacy
  • Source
  • Version
  • Contact

Jonkman Microblog is a social network, courtesy of SOBAC Microcomputer Services. It runs on GNU social, version 1.2.0-beta5, available under the GNU Affero General Public License.

Creative Commons Attribution 3.0 All Jonkman Microblog content and data are available under the Creative Commons Attribution 3.0 license.

Switch to desktop site layout.