Lectures on Intuitionistic Logic. Part 2

Abstract

Intuitionistic logic has become ubiquitous in computer science. An important question is how to teach intuitionistic logic to computer science and mathematics students. We attempted to begin such an exposition in Nerode 1989 using Kripke models which allow us to represent states of knowledge about machines. This document is an introduction, without proofs, to the semantics of recursive realizability and the Curry-Howard isomorphism. This is the subject behind term extraction functional computer languages such as ML or NuPRL. Partial Contents: Orientation; Logical deduction and computation; Instuitionistic natural deduction; Heyting's semantics; Set theory and application; Curry-Howard isomorphism; Typed combinators; Second order propositional calculus; Polymorphic lambda calculus. (KR)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1989
Accession Number
ADA213959

Entities

People

  • A. Nerode

Organizations

  • Cornell University

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Algorithms
  • Automata
  • Automata Theory
  • Computations
  • Computer Languages
  • Computer Programming
  • Computer Science
  • Computers
  • Language
  • Logic
  • Mathematical Logic
  • Mathematics
  • Numbers
  • Programming Languages
  • Recursive Functions
  • Set Theory
  • Theoretical Computer Science

Readers

  • Artificial Intelligence
  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.