{
  "id": "1102.1061",
  "version": "v2",
  "published": "2011-02-05T09:11:04.000Z",
  "updated": "2011-03-03T20:55:20.000Z",
  "title": "Continuation-passing Style Models Complete for Intuitionistic Logic",
  "authors": [
    "Danko Ilik"
  ],
  "doi": "10.1016/j.apal.2012.05.003",
  "categories": [
    "math.LO",
    "cs.LO",
    "cs.PL"
  ],
  "abstract": "A class of models is presented, in the form of continuation monads polymorphic for first-order individuals, that is sound and complete for minimal intuitionistic predicate logic. The proofs of soundness and completeness are constructive and the computational content of their composition is, in particular, a $\\beta$-normalisation-by-evaluation program for simply typed lambda calculus with sum types. Although the inspiration comes from Danvy's type-directed partial evaluator for the same lambda calculus, the there essential use of delimited control operators (i.e. computational effects) is avoided. The role of polymorphism is crucial -- dropping it allows one to obtain a notion of model complete for classical predicate logic. The connection between ours and Kripke models is made through a strengthening of the Double-negation Shift schema.",
  "revisions": [
    {
      "version": "v2",
      "updated": "2011-03-03T20:55:20.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03B20",
      "03B35",
      "03B40",
      "68N18",
      "03F55",
      "03F50",
      "03B55"
    ],
    "keywords": [
      "continuation-passing style models complete",
      "intuitionistic logic",
      "minimal intuitionistic predicate logic",
      "lambda calculus",
      "continuation monads polymorphic"
    ],
    "tags": [
      "journal article"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable",
      "adsabs": "2011arXiv1102.1061I"
    }
  }
}