1,721,042 research outputs found
Type Theory Should Eat Itself
No full textAbstractIn this paper I present a partial formalisation of a normaliser for type theory in Agda [Ulf Norell. Agda 2, 2007. http://www.cs.chalmers.se/~ulfn/]; extending previous work on big-step normalisation [Thorsten Altenkirch and James Chapman. Big-Step Normalisation. Journal of Functional Programming, 2008. Special Issue on Mathematically Structured Functional Programming. To appear, Thorsten Altenkirch and James Chapman. Tait in one big step. In Workshop on Mathematically Structured Functional Programming, MSFP 2006, Kuressaare, Estonia, July 2, 2006, electronic Workshop in Computing (eWiC), Kuressaare, Estonia, 2006. The British Computer Society (BCS)]. The normaliser in written as an environment machine. Only the computational behaviour of the normaliser is presented omitting details of termination
Front Matter, Table of Contents, Preface, Conference Organization
No full textThis volume contains the papers of the 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), which was held during 1-3 July 2015, in Warsaw, Poland
Big Step Normalisation for Type Theory
Get PDFBig step normalisation is a normalisation method for typed lambda-calculi which relies on a purely syntactic recursive evaluator. Termination of that evaluator is proven using a predicate called strong computability, similar to the techniques used to prove strong normalisation of β-reduction for typed lambda-calculi. We generalise big step normalisation to a minimalist dependent type theory. Compared to previous presentations of big step normalisation for e.g. the simply-typed lambda-calculus, we use a quotiented syntax of type theory, which crucially reduces the syntactic complexity introduced by dependent types. Most of the proof has been formalised using Agda
Towards a cubical type theory without an interval
Get PDFFollowing the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories start from a geometric view of equality. A proof of equality is encoded as a term in a context extended by the interval pretype. Our goal is to develop a cubical theory where the identity type is defined recursively over the type structure, and the geometry arises from these definitions. In this theory, cubes are present explicitly, e.g. a line is a telescope with 3 elements: two endpoints and the connecting equality. This is in line with Bernardy and Moulin's earlier work on internal parametricity. In this paper we present a naive syntax for internal parametricity and by replacing the parametric interpretation of the universe, we extend it to univalence. However, we don't know how to compute in this theory. As a second step, we present a version of the theory for parametricity with named dimensions which has an operational semantics. Extending this syntax to univalence is left as further work
Normalisation by evaluation for dependent types
Get PDFWe develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated using internal type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction. NBE for simple types is using a logical relation between the syntax and the presheaf interpretation. In our construction, we merge the presheaf interpretation and the logical relation into a proof-relevant logical predicate. We have formalized parts of the construction in Agda
A Syntactical Approach to Weak omega-Groupoids
No full textWhen moving to a Type Theory without proof-irrelevance the notion of a setoid has to be generalized to the notion of a weak omega-groupoid. As a first step in this direction we study the formalisation of weak omega-groupoids in Type Theory. This is motivated by Voevodsky's proposal of univalent type theory which is incompatible with proof-irrelevance and the results by Lumsdaine and Garner/van de Berg showing that the standard eliminator for equality gives rise to a weak omega-groupoid
To The Graduate School:
No full textce Foundation under Grant No. CCR-9985239. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation. Among the online resources I used are Google TM , CiteSeer, and LEO. I would like to thank everyone there for making their services available freely. Thorsten Altenkirch willingly answered my questions about [GHA01]. Natarajan Shankar provided me with some of his PVS files developed for [Sha96]. The L T E X template this thesis is based on was written by Thomas B ohne. I also want to thank him for proof-reading my thesis. Any remaining errors are of course my fault. Last but not least I would like to thank my parents Klaus and Frauke Weber for their great support over many, many years. v vi Contents List of Figures ix 1 Introduction 1 1.1 Objectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Organization . . . . . . .
Going Beyond Counting First Authors in Author Co-citation Analysis
Get PDFThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
- …
