View Item 
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        JavaScript is disabled for your browser. Some features of this site may not work without it.

        Browse

        All of UU Student Theses RepositoryBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

        The Curry-Howard isomorphism: A study of the computational content of intuitionistic and classical logic

        Thumbnail
        View/Open
        Thesis Jasmijn van Harskamp.pdf (597.1Kb)
        Publication date
        2020
        Author
        Harskamp, J. van
        Metadata
        Show full item record
        Summary
        The Curry-Howard isomorphism relates systems of formal logic to models of computation. It broadly states that proofs correspond to programs and formulae to types. For a long time it was believed the correspondence merely applied to intuitionistic logic. This changed when the axioms of classical logic were found to correspond to control operators. The correspondence is an important theoretical result connecting logic and computer science, but also has practical implications in e.g. program verification. This thesis will discuss the isomorphism with respect to both intuitionistic and classical logic. First, a language for the intuitionistic part of the correspondence will be constructed and assigned meaning by an operational semantics. These constructs will be used for exploring various aspects of the isomorphism, such as continuations and the relation between normalization and reduction. Subsequently, the language will be extended for a correspondence with classical logic by adding a control operator based on Peirce's law. The computational effects of this operator will be analysed and compared with other possible control operators, which arise from different classical axioms --i.e. a generalised version of Peirce's law, double negation elimination and the law of excluded middle. The correspondence will be shown to relate double negation embeddings of classical logic into intuitionistic logic to CPS translations. Finally, the complete language and semantics will be proven to have the properties of determinism, progress, preservation and termination.
        URI
        https://studenttheses.uu.nl/handle/20.500.12932/36496
        Collections
        • Theses
        Utrecht university logo