MiniML swMATH ID: 29625 Software Authors: Davies, Rowan; Pfenning, Frank Description: A modal analysis of staged computation. 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. Homepage: https://dl.acm.org/citation.cfm?doid=382780.382785 Keywords: binding times; run-time code generation; staged computation Related Software: Coq; ML; Haskell; Pesca; Links; Twelf; cubicaltt; Elf; Ynot; Agda; MetaOCaml; Nuprl; Automath; Polyp; Kleisli; Hop; Ur/Web; CDuce; Delphin; Freshml Cited in: 49 Publications all top 5 Cited by 74 Authors 5 Francez, Nissim 3 Bonelli, Eduardo 2 Birkedal, Lars 2 Clouston, Ranald A. 2 del Carmen González Huesca, Lourdes 2 Feller, Federico 2 Igarashi, Atsushi 2 Jay, C. Barry 2 Kamide, Norihiro 2 Kavvos, G. A. 2 Linares-Arévalo, P. Selene 2 Miranda Perea, Favio Ezequiel 2 Pfenning, Frank 2 Read, Stephen 2 Steren, Gabriela 1 Acar, Umut A. 1 Acclavio, Matteo 1 Alechina, Natasha 1 Angiuli, Carlo 1 Baratella, Stefano 1 Beklemishev, Lev D. 1 Berger, Martin J. 1 Bizjak, Aleš 1 Catta, Davide 1 Cerrito, Serenella 1 Charlton, Nathaniel 1 Costa Seco, João 1 Davies, Rowan 1 d’Avila Garcez, Artur S. 1 de Paiva, Valeria 1 Despeyroux, Joëlle 1 Dyckhoff, Roy 1 Farmer, William M. 1 Fatahalian, Kayvon 1 Feltman, Nicolas 1 Ferreira, Francisco H. G. 1 Fujita, Ken-etsu 1 Gabbay, Dov M. 1 Galmiche, Didier 1 Grathwohl, Hans Bugge 1 Gurevich, Yuri 1 Jacinto, Bruno 1 Kakutani, Yoshihiko 1 Kesner, Delia 1 Kimura, Daisuke 1 Kojima, Kensuke 1 Lamb, Luís C. 1 Liu, Yu David 1 Lourenço, Hugo 1 Lyon, Tim S. 1 Mannaa, Bassel 1 Masini, Andrea 1 Mendler, Michael 1 Møgelberg, Rasmus Ejlers 1 Perera, Roly 1 Pientka, Brigitte 1 Pitts, Andrew M. 1 Ranalter, Kurt 1 Reus, Bernhard 1 Ritter, Eike 1 Salhi, Yakoub 1 Scheele, Stephan 1 Schürmann, Carsten 1 Sheard, Tim 1 Shkatov, Dmitry 1 Skalka, Christian 1 Smith, Scott F. 1 Spitters, Bas 1 Straßburger, Lutz 1 Taha, Walid 1 Tratt, Laurence 1 Tsukada, Takeshi 1 Więckowski, Bartosz 1 Yang, Zhe all top 5 Cited in 18 Serials 6 Theoretical Computer Science 5 Information and Computation 3 Journal of Philosophical Logic 3 Logical Methods in Computer Science 2 Annals of Pure and Applied Logic 2 Journal of Logic and Computation 2 Journal of Applied Logic 2 Logica Universalis 1 Studia Logica 1 Bulletin of the Section of Logic 1 New Generation Computing 1 MSCS. Mathematical Structures in Computer Science 1 Journal of Logic, Language and Information 1 Journal of Applied Non-Classical Logics 1 Journal of Functional Programming 1 Journal of the ACM 1 Higher-Order and Symbolic Computation 1 RAIRO. Theoretical Informatics and Applications Cited in 3 Fields 37 Mathematical logic and foundations (03-XX) 26 Computer science (68-XX) 2 Category theory; homological algebra (18-XX) Citations by Year