×

Flag-based big-step semantics. (English) Zbl 1362.68160

Summary: Structural operational semantic specifications come in different styles: small-step and big-step. A problem with the big-step style is that specifying divergence and abrupt termination gives rise to annoying duplication. We present a novel approach to representing divergence and abrupt termination in big-step semantics using status flags. This avoids the duplication problem, and uses fewer rules and premises for representing divergence than previous approaches in the literature.

MSC:

68Q55 Semantics in the theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Agda; Paco; MiniAgda
PDFBibTeX XMLCite
Full Text: DOI arXiv Link

References:

[1] Plotkin, G. D., A structural approach to operational semantics, J. Log. Algebraic Program., 60-61, 17-139 (2004) · Zbl 1082.68062
[2] Kahn, G., Natural semantics, (STACS 87. STACS 87, Lect. Notes Comput. Sci., vol. 247 (1987), Springer), 22-39 · Zbl 0635.68007
[3] Leroy, X.; Grall, H., Coinductive big-step operational semantics, Inf. Comput., 207, 2, 284-304 (2009) · Zbl 1165.68044
[4] Nipkow, T.; Klein, G., Concrete Semantics: With Isabelle/HOL (2014), Springer · Zbl 1410.68004
[5] Hutton, G.; Wright, J., What is the meaning of these constant interruptions?, J. Funct. Program., 17, 777-792 (2007) · Zbl 1129.68410
[6] Danvy, O.; Nielsen, L. R., Refocusing in reduction semantics (2004), Dept. of Comp. Sci., Aarhus University, BRICS Research Series RS-04-26
[7] Bach Poulsen, C.; Mosses, P. D., Generating specialized interpreters for modular structural operational semantics, (LOPSTR’13. LOPSTR’13, Lect. Notes Comput. Sci., vol. 8901 (2014), Springer), 220-236 · Zbl 1453.68040
[8] Charguéraud, A., Pretty-big-step semantics, (ESOP’14. ESOP’14, Lect. Notes Comput. Sci., vol. 7792 (2013), Springer), 41-60 · Zbl 1381.68138
[9] Mosses, P. D., Modular structural operational semantics, J. Log. Algebraic Program., 60-61, 195-228 (2004) · Zbl 1072.68061
[10] Mosses, P. D.; New, M. J., Implicit propagation in structural operational semantics, Electron. Notes Theor. Comput. Sci., 229, 4, 49-66 (2009) · Zbl 1339.68159
[11] Reynolds, J. C., Definitional interpreters for higher-order programming languages, (ACM ’72, ACM Annual Conference (1972), ACM: ACM New York, NY, USA), 717-740
[12] Cousot, P.; Cousot, R., Inductive definitions, semantics and abstract interpretations, (POPL’92 (1992), ACM: ACM New York, NY, USA), 83-94
[13] Pierce, B. C., Types and Programming Languages (2002), MIT Press: MIT Press Cambridge, MA, USA · Zbl 0995.68018
[14] Sangiorgi, D., Introduction to Bisimulation and Coinduction (2011), Cambridge University Press: Cambridge University Press New York, NY, USA · Zbl 1252.68008
[15] Coquand, T.; Huet, G., The calculus of constructions, Inf. Comput., 76, 2-3, 95-120 (1988) · Zbl 0654.03045
[16] Pierce, B. C., Advanced Topics in Types and Programming Languages (2004), The MIT Press: The MIT Press Cambridge, MA, USA
[17] Seldin, J. P., On the proof theory of Coquand’s calculus of constructions, Ann. Pure Appl. Log., 83, 1, 23-101 (1997) · Zbl 0873.03048
[18] Pierce, B. C.; Casinghino, C.; Greenberg, M.; Hriţcu, C.; Sjöberg, V.; Yorgey, B., Software foundations (2013), electronic textbook
[19] Ciobâcă, Ş., From small-step semantics to big-step semantics, automatically, (IFM’13. IFM’13, Lect. Notes Comput. Sci., vol. 7940 (2013), Springer), 347-361
[20] Churchill, M.; Mosses, P. D.; Sculthorpe, N.; Torrini, P., Reusable components of semantic specifications, (Trans. Aspect-Oriented Software Development XII. Trans. Aspect-Oriented Software Development XII, Lect. Notes Comput. Sci., vol. 8989 (2015), Springer), 132-179
[21] Churchill, M.; Mosses, P. D., Modular bisimulation theory for computations and values, (FoSSaCS’13. FoSSaCS’13, Lect. Notes Comput. Sci., vol. 7794 (2013), Springer), 97-112 · Zbl 1260.68261
[22] Milner, R.; Tofte, M.; Harper, R.; MacQueen, D., The Definition of Standard ML (1997), MIT Press: MIT Press Cambridge, MA, USA
[23] Bach Poulsen, C.; Mosses, P. D., Deriving pretty-big-step semantics from small-step semantics, (ESOP’14. ESOP’14, Lect. Notes Comput. Sci., vol. 8410 (2014), Springer), 270-289 · Zbl 1405.68173
[24] Nakata, K.; Uustalu, T., Trace-based coinductive operational semantics for While, (TPHOLs’09. TPHOLs’09, Lect. Notes Comput. Sci., vol. 5674 (2009), Springer), 375-390 · Zbl 1252.68056
[25] Danielsson, N. A., Operational semantics using the partiality monad, (ICFP’12 (2012), ACM: ACM New York, NY, USA), 127-138 · Zbl 1291.68114
[26] Abel, A.; Chapman, J., Normalization by evaluation in the delay monad: a case study for coinduction via copatterns and sized types, MSFP’14. MSFP’14, Electron. Proc. Theor. Comput. Sci., 153, 51-67 (2014) · Zbl 1464.68050
[27] Piróg, M.; Gibbons, J., The coinductive resumption monad, Electron. Notes Theor. Comput. Sci., 308, 273-288 (2014) · Zbl 1337.68189
[28] Hancock, P.; Setzer, A., Interactive programs in dependent type theory, (CSL’00. CSL’00, Lect. Notes Comput. Sci., vol. 1862 (2000), Springer), 317-331 · Zbl 0973.68041
[29] Bove, A.; Dybjer, P.; Norell, U., A brief overview of Agda - a functional language with dependent types, (TPHOLs’09 (2009), Springer), 73-78 · Zbl 1252.68062
[30] Nakata, K.; Uustalu, T., Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction, SOS’10. SOS’10, Electron. Proc. Theor. Comput. Sci., 32, 57-75 (2010) · Zbl 1455.68100
[31] Hur, C.; Neis, G.; Dreyer, D.; Vafeiadis, V., The power of parameterization in coinductive proof, (POPL’13 (2013), ACM: ACM New York, NY, USA), 193-206 · Zbl 1301.68220
[32] Abel, A., MiniAgda: integrating sized and dependent types, PAR’10. PAR’10, Electron. Proc. Theor. Comput. Sci., 43, 14-28 (2010)
[33] Milner, R., Processes: a mathematical model of computing agents, Logic Colloquium ’73. Logic Colloquium ’73, Stud. Logic Found. Math., 80, 157-173 (1975) · Zbl 0316.68017
[34] Uustalu, T., Coinductive big-step semantics for concurrency, PLACES’13. PLACES’13, Electron. Proc. Theor. Comput. Sci., 137, 63-78 (2013)
[35] Owens, S.; Myreen, M. O.; Kumar, R.; Tan, Y. K., Functional big-step semantics, (ESOP’16. ESOP’16, Lect. Notes Comput. Sci., vol. 9632 (2016), Springer), 589-615
[36] Moggi, E., Notions of computation and monads, Inf. Comput., 93, 1, 55-92 (1991) · Zbl 0723.68073
[37] Cenciarelli, P.; Moggi, E., A syntactic approach to modularity in denotational semantics, (Category Theory and Computer Science, Proc. 5th Intl. Conf. (1993))
[38] Bach Poulsen, C.; Mosses, P. D.; Torrini, P., Imperative polymorphism by store-based types as abstract interpretations, (PEPM’15 (2015), ACM: ACM New York, NY, USA), 3-8
[39] Bach Poulsen, C., Extensible transition system semantics (2016), Swansea University, Ph.D. thesis
[40] Bahr, P.; Hutton, G., Calculating correct compilers, J. Funct. Program., 25, e14 (2015), (47 pages) · Zbl 1420.68053
[41] Leroy, X., Formal certification of a compiler back-end or: programming a compiler with a proof assistant, (POPL’06 (2006), ACM: ACM New York, NY, USA), 42-54 · Zbl 1369.68124
[42] Wright, A. K.; Felleisen, M., A syntactic approach to type soundness, Inf. Comput., 115, 1, 38-94 (1994) · Zbl 0938.68559
[43] Harper, R.; Stone, C., A type-theoretic interpretation of Standard ML, (Plotkin, G.; Stirling, C.; Tofte, M., Proof, Language, and Interaction (2000), MIT Press: MIT Press Cambridge, MA, USA), 341-387 · Zbl 0968.68018
[44] Cousot, P., Types as abstract interpretations, (POPL’97 (1997), ACM: ACM New York, NY, USA), 316-331
[45] Ager, M. S.; Biernacki, D.; Danvy, O.; Midtgaard, J., A functional correspondence between evaluators and abstract machines, (PPDP’03 (2003), ACM: ACM New York, NY, USA), 8-19
[46] Danvy, O.; Millikin, K., On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion, Inf. Process. Lett., 106, 3, 100-109 (2008) · Zbl 1186.68122
[47] Simmons, R. J.; Zerny, I., A logical correspondence between natural semantics and abstract machines, (PPDP’13 (2013), ACM: ACM New York, NY, USA), 109-119
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.