ﻻ يوجد ملخص باللغة العربية
We introduce a syntactic translation of Goedels System T parametrized by a weak notion of a monad, and prove a corresponding fundamental theorem of logical relation. Our translation structurally corresponds to Gentzens negative translation of classical logic. By instantiating the monad and the logical relation, we reveal the well-known properties and structures of T-definable functionals including majorizability, continuity and bar recursion. Our development has been formalized in the Agda proof assistant.
Type theories with higher-order subtyping or singleton types are examples of systems where computation rules for variables are affected by type information in the context. A complication for these systems is that bounds declared in the context do not
We characterise the sentences in Monadic Second-order Logic (MSO) that are over finite structures equivalent to a Datalog program, in terms of an existential pebble game. We also show that for every class C of finite structures that can be expressed
The intersection type assignment system has been designed directly as deductive system for assigning formulae of the implicative and conjunctive fragment of the intuitionistic logic to terms of lambda-calculus. But its relation with the logic is not
Normalization fails in type theory with an impredicative universe of propositions and a proof-irrelevant propositional equality. The counterexample to normalization is adapted from Girards counterexample against normalization of System F equipped wit
We present a system called Adelfa that provides mechanized support for reasoning about specifications developed in the Edinburgh Logical Framework or LF. Underlying Adelfa is a new logic named L_LF. Typing judgements in LF are represented by atomic f