Abstract
Type theory provides a formal basis for programming languages and can also be used to model reasoning systems such as Euler diagrams. We present part of a simple type theory of Euler diagrams. Expressing a system of reasoning with Euler diagrams as a collection of types and operations on types (which correspond to diagrams and reasoning rules) is a first step towards embedding visually modelled constraints directly into the type system of a programming language.
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
References
Altenkirch, T., Mcbride, C., Mckinna, J.: Why dependent types matter (2005) (accessed 01/02/08), http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf
Nordstrom, B., Petersson, K., Smith, J.M.: Programming in Martin-Löf’s Type Theory. OUP (1990)
Stapleton, G., Delaney, A.: Evaluating and generalizing constraint diagrams. Journal of Visual Languages and Computing (JVLC 2008)
Stapleton, G., Masthoff, J., Flower, J., Fish, A., Southern, J.: Automated theorem proving in Euler diagrams systems. Journal of Automated Reasoning 39, 431–470 (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Burton, J. (2008). Types and Programs from Euler Diagrams. In: Stapleton, G., Howse, J., Lee, J. (eds) Diagrammatic Representation and Inference. Diagrams 2008. Lecture Notes in Computer Science(), vol 5223. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87730-1_35
Download citation
DOI: https://doi.org/10.1007/978-3-540-87730-1_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87729-5
Online ISBN: 978-3-540-87730-1
eBook Packages: Computer ScienceComputer Science (R0)