Skip to main content
SpringerLink
Log in

Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic

  • Conference paper
Computer Science Logic (CSL 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6247))

Included in the following conference series:

Abstract

We prove ”untyping” theorems: in some typed theories (semirings, Kleene algebras, residuated lattices, involutive residuated lattices), typed equations can be derived from the underlying untyped equations. As a consequence, the corresponding untyped decision procedures can be extended for free to the typed settings. Some of these theorems are obtained via a detour through fragments of cyclic linear logic, and give rise to a substantial optimisation of standard proof search algorithms.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2(3), 297–347 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  2. Bellin, G., Fleury, A.: Planar and braided proof-nets for MLL with mix. Archive for Mathematical Logic 37, 309–325 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  3. Bellin, G., Scott, P.: On the π-calculus and linear logic. TCS 135, 11–65 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  4. Braibant, T., Pous, D.: Coq library: ATBR, algebraic tools for binary relations (May 2009), http://sardes.inrialpes.fr/~braibant/atbr/

  5. Braibant, T., Pous, D.: An efficient coq tactic for deciding Kleene algebras. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving. LNCS, vol. 6172, pp. 163–178. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  6. Burmeister, P.: Partial Algebra. In: Algebras and Orders. Kluwer Pub., Dordrecht (1993)

    Google Scholar 

  7. Diaconescu, R.: An encoding of partial algebras as total algebras. Information Processing Letters 109(23-24), 1245–1251 (2009)

    Article  MathSciNet  Google Scholar 

  8. Dojer, N.: Applying term rewriting to partial algebra theory. Fundamenta Informaticae 63(4), 375–384 (2004)

    MATH  MathSciNet  Google Scholar 

  9. Doornbos, H., Backhouse, R., van der Woude, J.: A calculational approach to mathematical induction. TCS 179(1-2), 103–135 (1997)

    Article  MATH  Google Scholar 

  10. Freyd, P., Scedrov, A.: Categories, Allegories. North-Holland, Amsterdam (1990)

    MATH  Google Scholar 

  11. Galatos, N., Jipsen, P., Kowalski, T., Ono, H.: Residuated lattices: an algebraic glimpse at substructural logics. Stud. in Log. and Found. of Math. 151, 532 (2007)

    MathSciNet  Google Scholar 

  12. Girard, J.-Y.: Linear logic. TCS 50, 1–102 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  13. Grégoire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98–113. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  14. Harrison, J.: A HOL decision procedure for elementary real algebra. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol. 780, pp. 426–435. Springer, Heidelberg (1994)

    Google Scholar 

  15. Jipsen, P.: Semirings to residuated Kleene lattices. Stud. Log. 76(2), 291–303 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  16. Jipsen, P., Tsinakis, C.: A survey of residuated lattices. Ord. Alg. Struct. (2002)

    Google Scholar 

  17. Kanovich, M.: The complexity of neutrals in linear logic. In: Proc. LICS, pp. 486–495. IEEE, Los Alamitos (1995)

    Google Scholar 

  18. Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Automata Studies, pp. 3–41. Princeton University Press, Princeton (1956)

    Google Scholar 

  19. Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation 110(2), 366–390 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  20. Kozen, D.: Kleene algebra with tests. Trans. PLS 19(3), 427–443 (1997)

    Google Scholar 

  21. Kozen, D.: Typed Kleene algebra. Technical Report 98-1669, Cornell Univ. (1998)

    Google Scholar 

  22. Krob, D.: Complete systems of B-rational identities. TCS 89(2), 207–343 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  23. Lambek, J.: The mathematics of sentence structure. American Mathematical Monthly 65, 154–170 (1958)

    Article  MATH  MathSciNet  Google Scholar 

  24. Mossakowski, T.: Relating CASL with other specification languages: the institution level. TCS 286(2), 367–475 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  25. Norrish, M.: Complete integer decision procedures as derived rules in HOL. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 71–86. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  26. Okada, M., Terui, K.: The finite model property for various fragments of intuitionistic linear logic. Journal of Symbolic Logic 64(2), 790–802 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  27. Ono, H., Komori, Y.: Logics without the contraction rule. Journal of Symbolic Logic 50(1), 169–201 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  28. Pentus, M.: Lambek calculus is NP-complete. TCS 357(1-3), 186–201 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  29. Pous, D.: Web appendix of this paper, http://sardes.inrialpes.fr/~pous/utas

  30. Pratt, V.R.: Action logic and pure induction. In: van Eijck, J. (ed.) JELIA 1990. LNCS, vol. 478, pp. 97–120. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  31. Regnier, L.: Lambda-calcul et réseaux. Thèse de doctorat, Univ. Paris VII (1992)

    Google Scholar 

  32. Wille, A.: A Gentzen system for involutive residuated lattices. Algebra Universalis 54, 449–463 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  33. Yetter, D.: Quantales and (noncommutative) linear logic. Journal of Symbolic Logic 55(1), 41–64 (1990)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CNRS (LIG, UMR 5217),  

    Damien Pous

Authors
  1. Damien Pous
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Laboratory, University of Cambridge, J.J. Thomson Avenue, CB3 0FD, Cambridge, UK

    Anuj Dawar

  2. Formal Methods in Systems Engineering, Vienna University of Technology, Favoritenstr. 9-11, 1040, Vienna, Austria

    Helmut Veith

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pous, D. (2010). Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic. In: Dawar, A., Veith, H. (eds) Computer Science Logic. CSL 2010. Lecture Notes in Computer Science, vol 6247. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15205-4_37

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15205-4_37

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15204-7

  • Online ISBN: 978-3-642-15205-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation