Abstract Davidsonian event semantics (Davidson 1967) is widely accepted as a powerful framework for formal semantics. It has brought about many benefits in semantic construction, which may be summarised into two categories: one is to provide a satisfactory solution to a seemingly intractable problem of variable polyadicity, and the other consists of those benefits that come from the availability of the entities called events that correspond to verb actions. This paper provides an analysis of event semantics from a general viewpoint of dependent type theory. First, it is shown that the problem of variable polyadicity can be solved by means of dependent typing, without the employment of events. To do this, we only extend the simple type theory with two type constructors and the resulting semantic definitions not only allow variable polyadicity as desired but also obtain logical inferences as expected. We shall discuss why the solution is natural from a type-theoretical point of view (as compared with that in set theory). We then discuss that most (if not all) of the other benefits of event semantics may already be obtained by alternative means without introducing events as ontological entities. To this end, we consider the evidence for event semantics discussed by Parsons (1990), focusing on two particular aspects: event talks and perception words, showing that the former is mostly concerned with timing, and the latter can be dealt with a special case without introducing events in general.

The shopping query suggestion offers personalized queries to users and plays a crucial role in search engines. However, existing shopping query suggestion methods suffer from poor task generalization and limited semantic comprehension problems. This paper presents a comprehensive framework for the shopping query suggestion that effectively addresses the shortcomings of existing approaches. Our proposed framework leverages a generative language model and fine-grained preference alignment to enhance semantic comprehension and improve the quality of generated queries. Our key contributions include the introduction of a personalized prompt set for diverse query suggestion tasks, the integration of interaction behavior time to capture user query interests, and the utilization of reinforcement learning techniques to align user preferences. Experimental results demonstrate enhancements in different scenarios. Our codes are available at https://github.com/1170300319/CIKM2024_SOUP.

We present a programme of research forpluralist formalisations, that is, formalisations that involve proving results in more than one foundation. A foundation consists of two parts: a logical part, which provides a notion of inference, and a non-logical part, which provides the entities to be reasoned about. An LTT is a formal system composed of two such separate parts. We show how LTTs may be used as the basis for a pluralist formalisation. We show how different foundations may be formalised as LTTs, and also describe a new method for proof reuse. If we know that a translation Φ exists between two logic-enriched type theories (LTTs)SandT, and we have formalised a proof of a theorem α inS, we may wish to make use of the fact that Φ(α) is a theorem ofT. We show how this is sometimes possible by writing a proof scriptMΦ. For any proof scriptMαthat proves a theorem α inS, if we changeMαso it first importsMΦ, the resulting proof script will still parse, and will be a proof of Φ(α) inT. In this paper, we focus on the logical part of an LTT-framework and show how the above method of proof reuse is done for four cases of Φ: inclusion, the double negation translation, theA-translation and the Russell–Prawitz modality. This work has been carried out using the proof assistant Plastic.

We construct a logic-enriched type theory LTT W that corresponds closely to the predicative system of foundations presented by Hermann Weyl in Das Kontinuum . We formalize many results from that book in LTT W , including Weyl's definition of the cardinality of a set and several results from real analysis, using the proof assistant Plastic that implements the logical framework LF. This case study shows how type theory can be used to represent a nonconstructive foundation for mathematics.

We incorporate the idea of coercive subtyping, a theory of abbreviation for dependent type theories, into the polymorphic type system in functional programming languages. The traditional type system with let-polymorphism is extended with argument coercions and function coercions, and a corresponding type inference algorithm is presented and proved to be sound and complete.

In this paper we study subtyping for inductive types in dependent type theories in the framework of coercive subtyping. General structural subtyping rules for parameterised inductive types are formulated based on the notion of inductive schemata. Certain extensional equality rules play an important role in proving some of the crucial properties of the type system with these subtyping rules. In particular, it is shown that the structural subtyping rules are coherent and that transitivity is admissible in the presence of the functorial rules of computational equality.

A lambda-free logical framework takes parameterisation and definitions as the basic notions to provide schematic mechanisms for specification of type theories and their use in practice. The framework presented here, PAL + , is a logical framework for specification and implementation of type theories, such as Martin-Löf's type theory or UTT. As in Martin-Löf's logical framework (Nordström et al. , 1990), computational rules can be introduced and are used to give meanings to the declared constants. However, PAL + only allows one to talk about the concepts that are intuitively in the object type theories: types and their objects, and families of types and families of objects of types. In particular, in PAL + , one cannot directly represent families of families of entities, which could be done in other logical frameworks by means of lambda abstraction. PAL + is in the spirit of de Bruijn's PAL + for Automath (de Bruijn, 1980). Compared with PAL, PAL + allows one to represent parametric concepts such as families of types and families of non-parametric objects, which can be used by themselves as totalities as well as when they are fully instantiated. Such parametric objects are represented by local definitions (let-expressions). We claim that PAL + is a correct meta-language for specifying type theories (e.g., dependent type theories), as it has the advantage of exactly capturing the intuitive concepts in object type theories, and that its implementation reflects the actual use of type theories in practice. We shall study the meta-theory of PAL + by developing its typed operational semantics and showing that it has nice meta-theoretic properties.

We propose and study coercive subtyping, a formal extension with subtyping of dependent type theories such as Martin-Löf's type theory and the type theory UTT. In this approach, subtyping with specified implicit coercions is treated as a feature at the level of the logical framework; in particular, the meaning of an object being in a supertype is given by coercive definition rules for the definitional equality. This provides a conceptually simple and uniform framework to understand subtyping and inheritance relations in type thoeries with sophisticated type structures such as inductive types and universes. The use of coercive subtyping in formal development and in reasoning about subsets of objects is discussed in the context of computer-assisted formal reasoning. Key words: Type theory, subypting, coercion, formal reasoning, logical framework.

The study of type theory may offer a uniform language for modular programming, structured specification and logical reasoning. We develop an approach to program specification and data refinement in a type theory with a strong logical power and nice structural mechanisms to show that it provides an adequate formalism for modular development of programs and specifications. Specification of abstract data types is considered, and a notion of abstract implementation between specifications is defined in the type theory and studied as a basis for correct and modular development of programs by stepwise refinement. The higher-order structural mechanisms in the type theory provide useful and flexible tools (specification operations and parameterized specifications) for modular design and structured specification. Refinement maps (programs and design decisions) and proofs of implementation correctness can be developed by means of the existing proof development systems based on type theories.

We present a higher-order calculus ECC which naturally combines Coquand-Huet's calculus of constructions and Martin-Löf's type theory with universes. ECC is very expressive, both for structured abstract reasoning and for program specification and construction. In particular, the strong sum types together with the type universes provide a useful module mechanism for abstract description of mathematical theories and adequate formalization of abstract mathematics. This allows comprehensive structuring of interactive development of specifications, programs and proofs. After a summary of the meta-theoretic properties of the calculus, an ω-Set (realizability) model of ECC is described to show how its essential properties can be captured set-theoretically. The model construction entails the logical consistency of the calculus and gives some hints on how to adequately formalize abstract mathematics. Theory abstraction in ECC is discussed as a pragmatic application.

A higher-order calculus ECC (extended calculus of constructions) is presented which can be seen as an extension of the calculus of constructions by adding strong sum types and a fully cumulative type hierarchy. ECC turns out to be rather expressive so that mathematical theories can be abstractly described and abstract mathematics may be adequately formalized. It is shown that ECC is strongly normalizing and has other nice proof-theoretic properties. An omega -set (realizability) model is described to show how the essential properties of the calculus can be captured set-theoretically.>