2001/05/01 by Rowan Davies, Frank Pfenning · 4 citations
Computer Science · #Logic, programming, and type systems #Logic, Reasoning, and Knowledge #Semantic Web and Ontologies #Correctness #Computer science #Programming language #Computation #Functional programming #Fragment (logic) #Modal #Context (archaeology) #Modal logic #Code (set theory) #Theoretical computer science #Algorithm
paper · doi:10.1145/382780.382785
openalex publication_date 2001/05/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/30
We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in the context of typed λ-calculi and functional languages. We directly demonstrate the sense in which our λ e →□ -calculus captures staging, and also give a conservative embeddng of Nielson and Nielson's two-level functional language in our functional language Mini-ML □ , thus proving that binding-time correctness is equivalent to modal correctness on this fragment. In addition, Mini-ML □ can also express immediate evaluation and sharing of code across multiple stages, thus supporting run-time code generation as well as partial evaluation.