Abstract:
We report on the idea to use colours to distinguish syntax and semantics as an educational tool in logic classes. This distinction gives also reason to reflect on some philosophical issues concerning semantics.

Abstract:
We give an algebraic characterization of the syntax and semantics of a class of simply-typed languages, such as the language PCF: we characterize simply-typed binding syntax equipped with reduction rules via a universal property, namely as the initial object of some category. For this purpose, we employ techniques developed in two previous works: in [2], we model syntactic translations between languages over different sets of types as initial morphisms in a category of models. In [1], we characterize untyped syntax with reduction rules as initial object in a category of models. In the present work, we show that those techniques are modular enough to be combined: we thus characterize simply-typed syntax with reduction rules as initial object in a category. The universal property yields an operator which allows to specify translations - that are semantically faithful by construction - between languages over possibly different sets of types. We specify a language by a 2-signature, that is, a signature on two levels: the syntactic level specifies the types and terms of the language, and associates a type to each term. The semantic level specifies, through inequations, reduction rules on the terms of the language. To any given 2-signature we associate a category of models. We prove that this category has an initial object, which integrates the types and terms freely generated by the 2-signature, and the reduction relation on those terms generated by the given inequations. We call this object the (programming) language generated by the 2-signature. [1] Ahrens, B.: Modules over relative monads for syntax and semantics (2011), arXiv:1107.5252, to be published in Math. Struct. in Comp. Science [2] Ahrens, B.: Extended Initiality for Typed Abstract Syntax. Logical Methods in Computer Science 8(2), 1-35 (2012)

Abstract:
Semantic feedback is an important source of information that a parser could use to deal with local ambiguities in syntax. However, it is difficult to devise a systematic communication mechanism for interactive syntax and semantics. In this article, I propose a variant of left-corner parsing to define the points at which syntax and semantics should interact, an account of grammatical relations and thematic roles to define the content of the communication, and a conflict resolution strategy based on independent preferences from syntax and semantics. The resulting interactive model has been implemented in a program called COMPERE and shown to account for a wide variety of psycholinguistic data on structural and lexical ambiguities.

Abstract:
In this thesis we give an algebraic characterization of the syntax and semantics of simply-typed languages. More precisely, we characterize simply-typed binding syntax equipped with reduction rules via a universal property, namely as the initial object of some category. We specify a language by a 2-signature ({\Sigma}, A), that is, a signature on two levels: the syntactic level {\Sigma} specifies the sorts and terms of the language, and associates a sort to each term. The semantic level A specifies, through inequations, reduction rules on the terms of the language. To any given 2-signature ({\Sigma}, A) we associate a category of "models" of ({\Sigma}, A). We prove that this category has an initial object, which integrates the terms freely generated by {\Sigma} and the reduction relation - on those terms - generated by A. We call this object the programming language generated by ({\Sigma}, A). Initiality provides an iteration principle which allows to specify translations on the syntax, possibly to a language over different sorts. Furthermore, translations specified via the iteration principle are by construction type-safe and faithful with respect to reduction. To illustrate our results, we consider two examples extensively: firstly, we specify a double negation translation from classical to intuitionistic propositional logic via the category-theoretic iteration principle. Secondly, we specify a translation from PCF to the untyped lambda calculus which is faithful with respect to reduction in the source and target languages. In a second part, we formalize some of our initiality theorems in the proof assistant Coq. The implementation yields a machinery which, when given a 2-signature, returns an implementation of its associated abstract syntax together with certified substitution operation, iteration operator and a reduction relation generated by the specified reduction rules.

Abstract:
A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear logic. A syntax and complete categorical semantics are developed, the latter in terms of (strict) indexed symmetric monoidal categories with comprehension. Various optional type formers are treated in a modular way. In particular, we will see that the historically much-debated multiplicative quantifiers and identity types arise naturally from categorical considerations. These new multiplicative connectives are further characterised by several identities relating them to the usual connectives from dependent type theory and linear logic. Finally, one important class of models, given by families with values in some symmetric monoidal category, is investigated in detail.

Abstract:
The goal of this paper is to offer a novel account on the Syntax and Semantics of Spanish Spatial Prepositions. This account is novel in at least three aspects. First, the account offers a unified syntactic analysis that covers understudied types of Spanish Spatial Prepositions (e.g. en el centro de, junto y a la izquierda de). Second, the account shows that such treatment can be extended to morphological phenomena, and can capture both their internal structure (e.g. de-bajo), and licensing patterns pertaining to argument demotion. The account also captures an alternation between "a-" (e.g. alante) and "de-" Prepositions (e.g. debajo), with respect to demotion, and is consistent with standard treatments of where-questions (dónde, in Spanish). Third, the account offers a "direct compositionality" semantic treatment, in which the interpretation of Spanish Spatial Prepositions is directly "read off" from their structure. This account is shown to capture all the semantic data discussed in the paper (argument demotion, interaction of Prepositions with Verbs, coordinated Prepositions), and to successfully extend previous accounts of this category.

Abstract:
We focus on the production of efficient descriptions of objects, actions and events. We define a type of efficiency, textual economy, that exploits the hearer's recognition of inferential links to material elsewhere within a sentence. Textual economy leads to efficient descriptions because the material that supports such inferences has been included to satisfy independent communicative goals, and is therefore overloaded in Pollack's sense. We argue that achieving textual economy imposes strong requirements on the representation and reasoning used in generating sentences. The representation must support the generator's simultaneous consideration of syntax and semantics. Reasoning must enable the generator to assess quickly and reliably at any stage how the hearer will interpret the current sentence, with its (incomplete) syntax and semantics. We show that these representational and reasoning requirements are met in the SPUD system for sentence planning and realization.

Abstract:
Herein, we present a structured syntax of minimotifs and their functional annotation. A syntax-based model of minimotif function with established minimotif sequence definitions was implemented using a relational database management system (RDBMS). To assess the usefulness of our standardized semantics, a series of database queries and stored procedures were used to classify SH3 domain binding minimotifs into 10 groups spanning 700 unique binding sequences.Our derived minimotif syntax is currently being used to normalize minimotif covalent chemistry and functional definitions within the MnM database. Analysis of SH3 binding minimotif data spanning many different studies within our database reveals unique attributes and frequencies which can be used to classify different types of binding minimotifs. Implementation of the syntax in the relational database enables the application of many different analysis protocols of minimotif data and is an important tool that will help to better understand specificity of minimotif-driven molecular interactions with proteins.Minimotifs (also called Short Linear Motifs [SLIMs]), are short peptide sequences which play important roles in many cellular functions [1-3]. Many minimotif databases such as Minimotif Miner (MnM), Eukaryotic Linear Motif (ELM), phospho.ELM, DOMINO, MEROPS, PepCyber and HPRD have cataloged more than a thousand minimotif entries and are expected to have significant growth in the near future [1,4-10]. Each of these databases model functional minimotifs in some capacity, often using individualized annotation schemes useful for the subset of minimotif data being managed. As the amount of minimotif data continues to grow, there are several expected advantages to be gained from the use of a standardized syntax. A standardized syntax will facilitate exchange of data with different minimotif databases. Likewise, a standardized syntax will allow integration with other non-motif databases enabling researchers to examine t

Abstract:
Third of a series of articles laying down the bases for classical first order model theory. Interpretation of a language in a universe set. Evaluation of a term in a universe. Truth evaluation of an atomic formula. Reassigning the value of a symbol in a given interpretation. Syntax and semantics of a non atomic formula are then defined concurrently (this point is explained in [16], 4.2.1). As a consequence, the evaluation of any w.f.f. string and the relation of logical implication are introduced. Depth of a formula. Definition of satisfaction and entailment (aka entailment or logical implication) relations, see [18] III.3.2 and III.4.1 respectively.

Abstract:
We give an algebraic characterization of the syntax and semantics of a class of languages with variable binding. We introduce a notion of 2-signature: such a signature specifies not only the terms of a language, but also reduction rules on those terms. To any 2-signature $S$ we associate a category of "models" of $S$. This category has an initial object, which integrates the terms freely generated by $S$, and which is equipped with reductions according to the inequations given in $S$. We call this initial object the language generated by $S$. Models of a 2--signature are built from relative monads and modules over such monads. Through the use of monads, the models---and in particular, the initial model---come equipped with a substitution operation that is compatible with reduction in a suitable sense. The initiality theorem is formalized in the proof assistant Coq, yielding a machinery which, when fed with a 2-signature, provides the associated programming language with reduction relation and certified substitution.