Logo del repository
  1. Home
 
Opzioni

A Framework for Typed HOAS and Semantics

MICULAN, Marino
•
SCAGNETTO, Ivan
2003
  • conference object

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.
DOI
10.1145/888251.888269
Archivio
http://hdl.handle.net/11390/738645
info:eu-repo/semantics/altIdentifier/scopus/2-s2.0-1242287811
http://dl.acm.org/citation.cfm?id=888269
Diritti
closed access
Soggetti
  • categorical metamodel...

  • initial algebra seman...

  • metalanguages for syn...

  • presheaf categorie

  • typed abstract syntax...

Visualizzazioni
22
Data di acquisizione
Apr 19, 2024
Vedi dettagli
google-scholar
Get Involved!
  • Source Code
  • Documentation
  • Slack Channel
Make it your own

DSpace-CRIS can be extensively configured to meet your needs. Decide which information need to be collected and available with fine-grained security. Start updating the theme to match your nstitution's web identity.

Need professional help?

The original creators of DSpace-CRIS at 4Science can take your project to the next level, get in touch!

Realizzato con Software DSpace-CRIS - Estensione mantenuta e ottimizzata da 4Science

  • Impostazioni dei cookie
  • Informativa sulla privacy
  • Accordo con l'utente finale
  • Invia il tuo Feedback