Abstract
This paper presents \(\mathsf {CoreFun}\), a typed reversible functional language, which seeks to reduce typed reversible functional programming to its essentials. We present a complete formal definition of the language, including its formal semantics and type system, the latter of which is based on a combined reasoning logical system of unrestricted and relevantly typed terms, and allows special support for ancillary (read-only) variables through its unrestricted fragment. We show how, in many cases, the type system provides the possibility to statically check for the reversibility of programs. Finally, we detail how higher-level language features such as variants and type classes may be incorporated into \(\mathsf {CoreFun}\) as syntactic sugar, such that \(\mathsf {CoreFun}\) may be used as a core language for a reversible functional language in a more modern style.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
A rank-1 polymorphic system may not instantiate type variables with polymorphic types.
References
Anderson, A.R., Belnap, N.D.: Entailment: The Logic of Relevance and Necessity, vol. 1. Princeton University Press, Princeton (1975)
Axelsen, H.B., Glück, R.: On reversible turing machines and their function universality. Acta Informatica 53(5), 509–543 (2016)
Dunn, J.M., Restall, G.: Relevance logic. In: Gabbay, D., Guenther, F. (eds.) Handbook of Philosophical Logic, 2nd edn., vol. 6, pp. 1–192. Springer, Dordrecht (2002). https://doi.org/10.1007/978-94-017-0460-1_1
Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50(1), 1–101 (1987)
Glück, R., Kaarsgaard, R.: A categorical foundation for structured reversible flowchart languages. In: Silva, A. (ed.) Mathematical Foundations of Programming Semantics (MFPS XXXIII). Electronic Notes in Theoretical Computer Science, vol. 336, pp. 155–171. Elsevier (2018)
Green, A.S., Lumsdaine, P.L., Ross, N.J., Selinger, P., Valiron, B.: Quipper: a scalable quantum programming language. In: Conference on Programming Language Design and Implementation, PLDI, PLDI 2013, pp. 333–342. ACM (2013)
Huffman, D.A.: Canonical forms for information-lossless finite-state logical machines. IRE Trans. Inf. Theory 5(5), 41–59 (1959)
James, R.P., Sabry, A.: Theseus: a high level language for reversible computing (2014), work in progress paper at RC 2014. www.cs.indiana.edu/~sabry/papers/theseus.pdf
Landauer, R.: Irreversibility and heat generation in the computing process. IBM J. Res. Dev. 5(3), 183–191 (1961)
Lecerf, Y.: Machines de Turing réversibles. Comptes Rendus Hebdomadaires des Séances de l’Académie des Sciences 257, 2597–2600 (1963)
Lutz, C., Derby, H.: Janus: a time-reversible language. A letter to R. Landauer (1986). http://tetsuo.jp/ref/janus.pdf
Pierce, B.C.: Types and Programming Languages, 1st edn. The MIT Press, Cambridge (2002)
Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)
Polakow, J.: Ordered Linear Logic and Applications. Ph.D. thesis. Carnegie Mellon University (2001)
Sabry, A., Valiron, B., Vizzotto, J.K.: From Symmetric pattern-matching to quantum control. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 348–364. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89366-2_19
Schordan, M., Jefferson, D., Barnes, P., Oppelstrup, T., Quinlan, D.: Reverse code generation for parallel discrete event simulation. In: Krivine, J., Stefani, J.-B. (eds.) RC 2015. LNCS, vol. 9138, pp. 95–110. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20860-2_6
Schultz, U.P., Laursen, J.S., Ellekilde, L.-P., Axelsen, H.B.: Towards a domain-specific language for reversible assembly sequences. In: Krivine, J., Stefani, J.-B. (eds.) RC 2015. LNCS, vol. 9138, pp. 111–126. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20860-2_7
Thomsen, M.K.: A functional language for describing reversible logic. In: Specification & Design Languages, FDL 2012, pp. 135–142. IEEE (2012)
Thomsen, M.K., Axelsen, H.B.: Interpretation and programming of the reversible functional language. In: Symposium on the Implementation and Application of Functional Programming Languages, IFL 2015, pp. 8:1–8:13. ACM (2016)
Wadler, P.: Linear types can change the world! In: IFIP TC 2 Working Conference on Programming Concepts and Methods, pp. 347–359. North Holland (1990)
Yokoyama, T., Axelsen, H.B., Glück, R.: Towards a reversible functional language. In: De Vos, A., Wille, R. (eds.) RC 2011. LNCS, vol. 7165, pp. 14–29. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29517-1_2
Yokoyama, T., Axelsen, H.B., GlĂĽck, R.: Fundamentals of reversible flowchart languages. Theor. Comput. Sci. (2015) (in Press), https://doi.org/10.1016/j.tcs.2015.07.046
Yokoyama, T., Glück, R.: A reversible programming language and its invertible self-interpreter. In: Partial Evaluation and Program Manipulation, PEPM 2007, pp. 144–153. ACM (2007)
Acknowledgements
This work was partly supported by the European COST Action IC 1405: Reversible Computation—Extending Horizons of Computing.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Jacobsen, P.A.H., Kaarsgaard, R., Thomsen, M.K. (2018). \(\mathsf {CoreFun}\): A Typed Functional Reversible Core Language. In: Kari, J., Ulidowski, I. (eds) Reversible Computation. RC 2018. Lecture Notes in Computer Science(), vol 11106. Springer, Cham. https://doi.org/10.1007/978-3-319-99498-7_21
Download citation
DOI: https://doi.org/10.1007/978-3-319-99498-7_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-99497-0
Online ISBN: 978-3-319-99498-7
eBook Packages: Computer ScienceComputer Science (R0)