A5070681215- Natural Language Processing Techniques
- Logic, programming, and type systems
- Topic Modeling
- Logic, Reasoning, and Knowledge
- Formal Methods in Verification
- Semantic Web and Ontologies
- Text Readability and Simplification
- Parallel Computing and Optimization Techniques
- Model-Driven Software Engineering Techniques
- Software Engineering Research
- Advanced Text Analysis Techniques
- semigroups and automata theory
- Advanced Database Systems and Queries
- Algorithms and Data Compression
- Advanced Software Engineering Methodologies
- Scientific Computing and Data Management
- Multi-Agent Systems and Negotiation
- Software Testing and Debugging Techniques
- Music and Audio Processing
- Bayesian Modeling and Causal Inference
- Speech Recognition and Synthesis
- Security and Verification in Computing
- Web Data Mining and Analysis
- Speech and Audio Processing
- Authorship Attribution and Profiling
University of Gothenburg
2013-2023
Chalmers University of Technology
2008-2016
Abstract Reynolds' abstraction theorem (Reynolds, J. C. (1983) Types, and parametric polymorphism, Inf. Process. 83 (1), 513–523) shows how a typing judgement in System F can be translated into relational statement (in second-order predicate logic) about inhabitants of the type. We obtain similar result for pure type systems (PTSs): any PTS used as programming language, there is that logic parametricity. Types source are to relations (expressed types) target. Similarly, values given proofs...
The Universal Morphology (UniMorph) project is a collaborative effort providing broad-coverage instantiated normalized morphological inflection tables for hundreds of diverse world languages. comprises two major thrusts: language-independent feature schema rich annotation and type-level resource annotated data in languages realizing that schema. This paper presents the expansions improvements made on several fronts over last couple years (since McCarthy et al. (2020)). Collaborative efforts...
We consider the extent to which different deep neural network (DNN) configurations can learn syntactic relations, by taking up Linzen et al.’s (2016) work on subject-verb agreement with LSTM RNNs. test their methods a much larger corpus than they used (a ⇠24 million example part of WaCky corpus, instead ⇠1.35 both drawn from Wikipedia). experiment several DNN architectures (LSTM RNNs, GRUs, and CNNs), alternative parameter settings for these systems (vocabulary size, training ratio, number...
We propose to unify the treatment of a broad range modalities in typed lambda calculi. do so by defining generic structure modalities, and show that this arises naturally from intuitionistic logic, as such finds instances wide type systems previously described literature. Despite generality, has rich metatheory, which we expose.
Tiago Pimentel, Maria Ryskina, Sabrina J. Mielke, Shijie Wu, Eleanor Chodroff, Brian Leonard, Garrett Nicolai, Yustinus Ghanggo Ate, Salam Khalifa, Nizar Habash, Charbel El-Khaissi, Omer Goldman, Michael Gasser, William Lane, Matt Coler, Arturo Oncevay, Jaime Rafael Montoya Samame, Gema Celeste Silva Villegas, Adam Ek, Jean-Philippe Bernardy, Andrey Shcherbakov, Aziyana Bayyr-ool, Karina Sheifer, Sofya Ganieva, Matvey Plugaryov, Elena Klyachko, Ali Salehi, Andrew Krizhanovsky, Natalia Clara...
Reynolds' abstraction theorem shows how a typing judgement in System F can be translated into relational statement (in second order predicate logic) about inhabitants of the type. We obtain similar result for single lambda calculus (a pure type system), which terms, types and their relations are expressed. Working within system dispenses with need an interpretation layer, allowing unusually simple presentation. While unification puts some constraints on (which we spell out), applies to many...
Linear type systems have a long and storied history, but not clear path forward to integrate with existing languages such as OCaml or Haskell. In this paper, we study linear system designed two crucial properties in mind: backwards-compatibility code reuse across non-linear users of library. Only then can the benefits types permeate conventional functional programming. Rather than bifurcate into counterparts, instead attach linearity function arrows. functions receive inputs from...
We extend Martin-Löf's Logical Framework with special constructions and typing rules providing internalized parametricity. Compared to previous similar proposals, this version comes a denotational semantics which is refinement of the standard presheaf dependent type theory. Further, one used interpret nominal sets restrictions. The present calculus candidate for core proof assistant
Abstract The tensor notation used in several areas of mathematics is a useful one, but it not widely available to the functional programming community. In practical sense, (embedded) domain-specific languages ( dsl s) that are currently use for algebra either 1. array-oriented do enforce or take advantage properties and algebraic structure 2. follow categorical tensors require programmer manipulate an unwieldy point-free notation. A deeper issue calculus, dominant pedagogical paradigm...

 Context-free grammars (CFG) were one of the first formal tools used to model natural languages, and they remain relevant today as basis several frameworks. A key ingredient CFG is presence nested recursion. In this paper, we investigate experimentally capability recurrent neural networks (RNNs) learn More precisely, measure an upper bound their do so, by simplifying task learning a generalized Dyck language, namely composed matching parentheses various kinds. To present RNNs with set...
Reynolds' abstraction theorem has recently been extended to lambda-calculi with dependent types. In this paper, we show how can be internalized. More precisely, describe an extension of the Pure Type Systems a special parametricity rule (with computational content), and prove fundamental properties such as Church-Rosser's strong normalization. All instances both expressed proved in calculus itself. Moreover, one apply rule: is itself parametric.
Dependent type-theory aims to become the standard way formalize mathematics at same time as displacing traditional platforms for high-assurance programming. However, current implementations of type theory are still lacking, in sense that some obvious truths require explicit proofs, making awkward use many applications, both formalization and In particular, notions erasure poorly supported.
Earlier studies have introduced a list of high-level evaluation criteria to assess how well language supports generic programming. Since each that meets all is considered generic, those are not fine-grained enough differentiate between languages for We refine these into taxonomy captures differences type classes in Haskell and concepts C++, discuss which incidental ones due other features. The allows an improved understanding support programming, the comparison useful ongoing discussions...
In this paper, we look at Natural Language Inference, arguing that the notion of inference current NLP systems are learning is much narrower compared to range patterns found in human reasoning. We take a history and nature creating datasets for NLI. discuss mainly used today relevant tasks show why those not enough generalize other reasoning tasks, e.g. logical legal reasoning, or dialogue settings. then proceed propose ways which can be remedied, effectively producing more realistic Lastly,...
Valiant (1975) has developed an algorithm for recognition of context free languages. As today, it remains the with best asymptotic complexity this purpose. In paper, we present algebraic specification, implementation, and proof correctness a generalisation Valiant's algorithm. The can be used recognition, parsing or generic calculation transitive closure upper triangular matrices. is certified by Agda assistant. certification representative state-of-the-art methods specification proofs in...
In this paper we revisit the connection between parametricity and noninterference. Our primary contribution is a proof of noninterference for polyvariant variation Dependency Core Calculus in Constructions. The modular: it leverages Constructions encoding data abstraction using existential types. This perspective gives rise to simple understandable proofs from parametricity. All our contributions have been mechanised Agda assistant.
This paper seeks to examine the effect of including background knowledge in form character pre-trained neural language model (LM), and data bootstrapping overcome problem unbalanced limited resources. As a test, we explore task identification mixed-language short non-edited texts with an under-resourced language, namely case Algerian Arabic for which both labelled unlabelled are limited. We compare performance two traditional machine learning methods deep networks (DNNs) model. The results...
We explore the effect of injecting background knowledge to different deep neural network (DNN) configurations in order mitigate problem scarcity annotated data when applying these models on datasets low-resourced languages. The is encoded form lexicons and pre-trained sub-word embeddings. DNN are evaluated task detecting code-switching borrowing points non-standardised user-generated Algerian texts. Overall results show that DNNs benefit from adding knowledge. However, gain varies between...