Software Search - zbMATH Open

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

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

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

37	Mathematical logic and foundations (03-XX)
26	Computer science (68-XX)
2	Category theory; homological algebra (18-XX)