1990/01/01 by Timothy G. Griffin · 7 citations
Computer Science · Mathematics · #Algebra over a field #Artificial intelligence #Calculus (dental) #Class (philosophy) #Computer science #Construct (python library) #Constructive #Constructive proof #Context (archaeology) #Continuation #Current (fluid) #Discrete mathematics #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematical proof #Mathematics #Programming language #Pure mathematics #Scheme (mathematics) #Theoretical computer science #Type (biology) #Type theory
paper · doi:10.1145/96709.96714
openalex publication_date 1990/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/29
The programming language Scheme contains the control construct call/cc that allows access to the current continuation (the current control context). This, in effect, provides Scheme with first-class labels and jumps. We show that the well-known formulae-as-types correspondence, which relates a constructive proof of a formula α to a program of type α, can be extended to a typed Idealized Scheme. What is surprising about this correspondence is that it relates classical proofs to typed programs. The existence of computationally interesting “classical programs” —programs of type α, where α holds classically, but not constructively — is illustrated by the definition of conjunctively, disjunctive, and existential types using standard classical definitions. We also prove that all evaluations of typed terms in Idealized Scheme are finite.