Skip to main content
SpringerLink
Log in

Encoding Generic Judgments

  • Conference paper
  • First Online:
FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2556))

Abstract

The operational semantics of a computation system is often presented as inference rules or, equivalently, as logical theories. Specifications can be made more declarative and high-level if syntactic details concerning bound variables and substitutions are encoded directly into the logic using term-level abstractions (λ-abstraction) and proof-level abstractions (eigenvariables). When one wishes to reason about relations defined using term-level abstractions, generic judgment are generally required. Care must be taken, however, so that generic judgments are not uniformly handled using proof-level abstractions. Instead, we present a technique for encoding generic judgments and show two examples where generic judgments need to be treated at the term level: one example is an interpreter for Horn clauses extended with universal quantified bodies and the other example is that of the π-calculus.

An earlier draft of this paper appeared in MERLIN 2001 [Mil01].

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. Jawahar Chirimar. Proof Theoretic Approach to Specification Languages. PhD thesis, University of Pennsylvania, February 1995.

    Google Scholar 

  2. Jolle Despeyroux. A higher-order specification of the π-calculus. In Proc. of the IFIP International Conference on Theoretical Computer Science, IFIP TCS’2000, Sendai, Japan, August 17–19, 2000., August 2000.

    Google Scholar 

  3. M. P. Fiore, G. D. Plotkin, and D. Turi. Abstract syntax and variable binding. In 14th Annual Symposium on Logic in Computer Science, pages 193–202. IEEE Computer Society Press, 1999.

    Google Scholar 

  4. Jean-Yves Girard. A fixpoint theorem in linear logic. Email to the linear@cs.stanford.edu mailing list, February 1992.

    Google Scholar 

  5. M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax involving binders. In 14th Annual Symposium on Logic in Computer Science, pages 214–224. IEEE Computer Society Press, 1999.

    Google Scholar 

  6. Furio Honsell, Marino Miculan, and Ivan Scagnetto. Pi-calculus in (co)inductive type theory. TCS, 253(2):239–285, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  7. M. Hofmann. Semantical analysis of higher-order abstract syntax. In 14th Annual Symposium on Logic in Computer Science, pages 204–213. IEEE Computer Society Press, 1999.

    Google Scholar 

  8. Lars Hallnäs and Peter Schroeder-Heister. A proof-theoretic approach to logic programming. ii. Programs as definitions. Journal of Logic and Computation, 1(5):635–660, October 1991.

    Article  MATH  MathSciNet  Google Scholar 

  9. Gérard Huet. A unification algorithm for typed λ-calculus. TCS, 1:27–57, 1975.

    Article  MathSciNet  Google Scholar 

  10. Gilles Kahn. Natural semantics. In Proc. of the Symposium on Theoretical Aspects of Computer Science, volume 247 of LNCS, pages 22–39. March 1987.

    Google Scholar 

  11. Raymond McDowell. Reasoning in a Logic with Definitions and Induction. PhD thesis, University of Pennsylvania, December 1997.

    Google Scholar 

  12. Dale Miller. Abstractions in logic programming. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 329–359. Academic Press, 1990.

    Google Scholar 

  13. Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  14. Dale Miller. Unification of simply typed lambda-terms as logic programming. In Eighth International Logic Programming Conference, pages 255–269, Paris, France, June 1991. MIT Press.

    Google Scholar 

  15. Dale Miller. Forum: A multiple-conclusion specification language. TCS, 165(1):201–232, September 1996.

    Article  MATH  Google Scholar 

  16. Dale Miller. Abstract syntax for variable binders: An overview. In John Lloyd and et. al., editors, Computational Logic-CL 2000, number 1861 in LNAI, pages 239–253. Springer, 2000.

    Google Scholar 

  17. Dale Miller. Encoding generic judgments: Preliminary results. In R.L. Crole S.J. Ambler and A. Momigliano, editors, ENTCS, volume 58. Elsevier, 2001. Proceedings of the MERLIN 2001 Workshop, Siena.

    Google Scholar 

  18. Raymond McDowell and Dale Miller. A logic for reasoning with higher-order abstract syntax. In Glynn Winskel, editor, Proceedings, Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 434–445, Warsaw, Poland, July 1997. IEEE Computer Society Press.

    Google Scholar 

  19. Raymond McDowell and Dale Miller. Cut-elimination for a logic with definitions and induction. TCS, 232:91–119, 2000.

    Article  MATH  MathSciNet  Google Scholar 

  20. Raymond McDowell and Dale Miller. Reasoning with higher-order abstract syntax in a logical framework. ACM Transactions on Computational Logic, 3(1):80–136, January 2002.

    Article  MathSciNet  Google Scholar 

  21. Raymond McDowell, Dale Miller, and Catuscia Palamidessi. Encoding transition systems in sequent calculus. TCS, 197(1–2), 2001. To appear.

    Google Scholar 

  22. Dale Miller and Gopalan Nadathur. A computational logic approach to syntax and semantics. Presented at the Tenth Symposium of the Mathematical Foundations of Computer Science, IBM Japan, May 1985.

    Google Scholar 

  23. Dale Miller and Gopalan Nadathur. Some uses of higher-order logic in computational linguistics. In Proceedings of the 24th Annual Meeting of the Association for Computational Linguistics, pages 247–255. Association for Computational Linguistics, Morristown, New Jersey, 1986.

    Google Scholar 

  24. Dale Miller and Gopalan Nadathur. A logic programming approach to manipulating formulas and programs. In Seif Haridi, editor, IEEE Symposium on Logic Programming, pages 379–388, San Francisco, September 1987.

    Google Scholar 

  25. Dale Miller and Catuscia Palamidessi. Foundational aspects of syntax. In Pierpaolo Degano, Roberto Gorrieri, Alberto Marchetti-Spaccamela, and Peter Wegner, editors, ACM Computing Surveys Symposium on Theoretical Computer Science: A Perspective, volume 31. ACM, Sep 1999.

    Google Scholar 

  26. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, Part II. Information and Computation, pages 41–77, 1992.

    Google Scholar 

  27. Tobias Nipkow. Higher-order critical pairs. In G. Kahn, editor, LICS91, pages 342–349. IEEE, July 1991.

    Google Scholar 

  28. Gopalan Nadathur and Dustin J. Mitchell. System description: Teyjus—a compiler and abstract machine based implementation of Lambda Prolog. In H. Ganzinger, ed., CADE16, pages 287–291, Trento, Italy, July 1999. LNCS.

    Google Scholar 

  29. Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363–397, September 1989.

    Google Scholar 

  30. Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pages 199–208. ACM Press, June 1988.

    Google Scholar 

  31. G. Plotkin. A structural approach to operational semantics. DAIMI FN-19, Aarhus University, Aarhus, Denmark, September 1981.

    Google Scholar 

  32. C. Röckl, D. Hirschko., and S. Berghofer. Higher-order abstract syntax with induction in Isabelle/HOL: Formalizing the pi-calculus and mechanizing the theory of contexts. In Proceedings of FOSSACS’01, LNCS, 2001.

    Google Scholar 

  33. Davide Sangiorgi. π-calculus, internal mobility and agent-passing calculi. TCS, 167(2):235–274, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  34. Peter Schroeder-Heister. Cut-elimination in logics with definitional reflection. In D. Pearce and H. Wansing, editors, Nonclassical Logics and Information Processing, volume 619 of LNCS, pages 146–171. Springer, 1992.

    Chapter  Google Scholar 

  35. Peter Schroeder-Heister. Rules of definitional reflection. In M. Vardi, editor, Eighth Annual Symposium on Logic in Computer Science, pages 222–232. IEEE Computer Society Press, IEEE, June 1993.

    Google Scholar 

  36. Alwen F. Tiu. An extension of L-lambda unification. Draft, available via http://www.cse.psu.edu/~tiu/llambdaext.pdf, September 2002.

  37. Jérémie D. Wajs. Reasoning about Logic Programs Using Definitions and Induction. PhD thesis, Pennsylvania State University, 2002.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA-FUTURS and Ècole Polytechnique, France

    Dale Miller

  2. Pennsylvania State University and Ècole Polytechnique, Pennsylvania

    Alwen Tiu

Authors
  1. Dale Miller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alwen Tiu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, Indian Institute of Technology, 208016, Kanpur, India

    Manindra Agrawal  & Anil Seth  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Miller, D., Tiu, A. (2002). Encoding Generic Judgments. In: Agrawal, M., Seth, A. (eds) FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2002. Lecture Notes in Computer Science, vol 2556. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36206-1_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-36206-1_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00225-3

  • Online ISBN: 978-3-540-36206-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation