A framework for typed HOAS and semantics

ABSTRACT

We investigate a framework for representing and reasoning about syntactic and semantic aspects of typed languages with variable binders.First, we introduce typed binding signatures and develop a theory of typed abstract syntax with binders. Each signature is associated to a category of "presentation" models, where the language of the typed signature is the initial model.At the semantic level, types can be given also a computational meaning in a (possibly different) semantic category. We observe that in general, semantic aspects of terms and variables can be reflected in the presentation category by means of an adjunction. Therefore, the category of presentation models is expressive enough to represent both the syntactic and the semantic aspects of languages.We introduce then a metalogical system, inspired by the internal languages of the presentation category, which can be used for reasoning on both the syntax and the semantics of languages. This system is composed by a core equational logic tailored for reasoning on the syntactic aspects; when a specific semantics is chosen, the system can be modularly extended with further "semantic" notions, as needed.

REFERENCES

• 1: A. Bucalo, M. Hofmann, F. Honsell, M. Miculan, and I. Scagnetto. Consistency of the theory of contexts. Submitted, 2001.
• 2: Marcelo Fiore , Daniele Turi, Semantics of Name and Value Passing, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.93, June 16-19, 2001
• 3: Marcelo Fiore, Semantic analysis of normalisation by evaluation for typed lambda calculus, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.26-37, October 06-08, 2002, Pittsburgh, PA, USA [doi>10.1145/571157.571161]
• 4: Marcelo Fiore , Gordon Plotkin , Daniele Turi, Abstract Syntax and Variable Binding, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.193, July 02-05, 1999
• 5: FreshML: A fresh approach to name binding in metaprogramming languages. http://www.cl.cam.ac.uk/~amp12/research/freshml/, 2002. Research project.
• 6: Murdoch Gabbay , Andrew Pitts, A New Approach to Abstract Syntax Involving Binders, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.214, July 02-05, 1999
• 7: Martin Hofmann, Semantical Analysis of Higher-Order Abstract Syntax, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.204, July 02-05, 1999
• 8: Furio Honsell , Marino Miculan , Ivan Scagnetto, An Axiomatic Approach to Metareasoning on Nominal Algebras in HOAS, Proceedings of the 28th International Colloquium on Automata, Languages and Programming,, p.963-978, July 08-12, 2001
• 9: Furio Honsell , Marino Miculan , Ivan Scagnetto, &pgr;-calculus in (Co)inductive-type theory, Theoretical Computer Science, v.253 n.2, p.239-285, Feb. 28, 2001 [doi>10.1016/S0304-3975(00)00095-5 ]
• 10: INRIA. The Coq Proof Assistant, 2002. http://coq.inria.fr/doc/main.html.
• 11: B. Jacobs. Categorical Logic and Type Theory, volume 141 of Studies in Logic and the Foundations of Mathematics. Elsevier, 1999.
• 12: G. Longo, editor. Proceedings, Fourteenth Annual IEEE Symposium on Logic in Computer Science, 1999. IEEE Computer Society Press.
• 13: S. Mac Lane. Categories for the Working Mathematician. Springer-Verlag, Berlin, 1971.
• 14: S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic: a First Introduction to Topos Theory. Universitext. Springer-Verlag, 1994.
• 15: Raymond McDowell , Dale Miller, A Logic for Reasoning with Higher-Order Abstract Syntax, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.434, June 29-July 02, 1997
• 16: Eugenio Moggi, Notions of computation and monads, Information and Computation, v.93 n.1, p.55-92, July 1991 [doi>10.1016/0890-5401(91)90052-4]
• 17: B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin-Löf's Type Theory: An Introduction, volume 7 of International Series of Monograph on Computer Science. Oxford University Press, 1990.
• 18: Andrew M. Pitts, Categorical logic, Handbook of logic in computer science: Volume 5: Logic and algebraic methods, Oxford University Press, Oxford, 2001
• 19: Andrew M. Pitts, Nominal Logic: A First Order Theory of Names and Binding, Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, p.219-242, October 29-31, 2001
• 20: Carsten Schürmann, Recursion for Higher-Order Encodings, Proceedings of the 15th International Workshop on Computer Science Logic, p.585-599, September 10-13, 2001

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Algebraic approaches to semantics; Denotational semantics
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Algebraic language theory

General Terms:
Languages, Theory

Keywords:
categorical metamodels, initial algebra semantics, metalanguages for syntax and semantics of languages, presheaf categories, typed abstract syntax with variable binding