| 1. |
- Stemle, Egon, et al.
(författare)
-
Working together towards an ideal infrastructure for language learner corpora
- 2019
-
Ingår i: Widening the Scope of Learner Corpus Research. Selected papers from the fourth Learner Corpus Research Conference. Corpora and Language in Use – Proceedings 5 / Andrea Abel, Aivars Glaznieks, Verena Lyding and Lionel Nicolas (eds.). - Louvain-la-Neuve : PUL, Presses Universitaires de Louvain. - 2034-6417. - 9782875588685
-
Konferensbidrag (refereegranskat)abstract
- In this article we provide an overview of first-hand experiences and vantage points for best practices from projects in seven European countries dedicated to learner corpus research (LCR) and the creation of language learner corpora. The corpora and tools involved in LCR are becoming more and more important, as are careful preparation and easy retrieval and reusability of corpora and tools. But the lack of commonly agreed solutions for many aspects of LCR, interoperability between learner corpora and the exchange of data from different learner corpus projects remains a challenge. We show how concepts like metadata, anonymization, error taxonomies and linguistic annotations as well as tools, toolchains and data formats can be individually challenging and how the challenges can be solved.
|
|
| 2. |
- Bernardy, Jean-Philippe, 1978, et al.
(författare)
-
Compiling Linear Logic using Continuations
- 2014
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- As System F is the logical foundation of functional programming, it haslong been expected that Classical Linear Logic (CLL) is the logicalfoundation of concurrent programming. In particular, thanks to aninvolutive negation, its language of propositions correspond to protocols.This means that CLL provides the principles to integrate concurrency intofunctional programming languages.Aiming towards this integration, we translate the concurrency features ofCLL into continuations, essentially via a negation-model of CLL into SystemF. Practically, the translation can be used to embed CLL programs intofunctional languages such as Haskell. We explain the properties of theinterface between the two languages. In particular, using an example, weillustrate how the par (⅋) operator can solve practical functionalprogramming problems.
|
|
| 3. |
- Borin, Lars, 1957, et al.
(författare)
-
Sparv: Språkbanken’s corpus annotation pipeline infrastructure
- 2016
-
Ingår i: SLTC 2016. The Sixth Swedish Language Technology Conference, Umeå University, 17-18 November, 2016.
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- Sparv is Språkbanken's corpus annotation pipeline infrastructure. The easiest way to use the pipeline is from its web interface with a plain text document. The pipeline uses in-house and external tools on the text to segment it into sentences and paragraphs, tokenise, tag parts-of-speech, look up in dictionaries and analyse compounds. The pipeline can also be run using a web API with XML results, and it is run locally at Språkbanken to prepare the documents in Korp, our corpus search tool. While the most sophisticated support is for modern Swedish, the pipeline supports 15 languages.
|
|
| 4. |
|
|
| 5. |
- Johansson, Moa, 1981, et al.
(författare)
-
Hipster: Integrating theory exploration in a proof assistant
- 2014
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319084336 ; 8543, s. 108-122
-
Konferensbidrag (refereegranskat)abstract
- This paper describes Hipster, a system integrating theory exploration with the proof assistant Isabelle/HOL. Theory exploration is a technique for automatically discovering new interesting lemmas in a given theory development. Hipster can be used in two main modes. The first is exploratory mode, used for automatically generating basic lemmas about a given set of datatypes and functions in a new theory development. The second is proof mode, used in a particular proof attempt, trying to discover the missing lemmas which would allow the current goal to be proved. Hipster's proof mode complements and boosts existing proof automation techniques that rely on automatically selecting existing lemmas, by inventing new lemmas that need induction to be proved. We show example uses of both modes.
|
|
| 6. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
Automating Inductive Proofs using Theory Exploration
- 2013
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783642385735 ; 7898, s. 392-406
-
Konferensbidrag (refereegranskat)abstract
- HipSpec is a system for automatically deriving and proving properties about functional programs. It uses a novel approach, combining theory exploration, counterexample testing and inductive theorem proving. HipSpec automatically generates a set of equational theorems about the available recursive functions of a program. These equational properties make up an algebraic specification for the program and can in addition be used as a background theory for proving additional user-stated properties. Experimental results are encouraging: HipSpec compares favourably to other inductive theorem provers and theory exploration systems.
|
|
| 7. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
SAT modulo intuitionistic implications
- 2015
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783662488980 ; 9450, s. 622-637
-
Konferensbidrag (refereegranskat)abstract
- We present a new method for solving problems in intuitionistic propositional logic, which involves the use of an incremental SAT-solver. The method scales to very large problems, and fits well into an SMT-based framework for interaction with other theories.
|
|
| 8. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
TIP: Tons of Inductive Problems
- 2015
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319206158 ; 9150, s. 332-336
-
Konferensbidrag (refereegranskat)abstract
- This paper describes our collection of benchmarks for inductive theorem provers. The recent spur of interest in automated inductive theorem proving has increased the demands for evaluation and comparison between systems. We expect the benchmark suite to continually grow as more problems are submitted by the community. New challenge problems will promote further development of provers which will greatly benefit both developers and users of inductive theorem provers.
|
|
| 9. |
- Malm, Per, et al.
(författare)
-
Uneek: a Web Tool for Comparative Analysis of Annotated Texts
- 2018
-
Ingår i: Proceedings of the LREC 2018 Workshop International FrameNetWorkshop 2018: Multilingual Framenets and Constructicons, 7-12 May 2018, Miyazaki (Japan) / [ed] Tiago Timponi Torrent, Lars Borin & Collin F. Baker, 2018. - 9791095546047
-
Konferensbidrag (refereegranskat)abstract
- In this paper, we present Uneek, a web based linguistic tool that performs set operations on raw or annotated texts. The tool may be used for automatic distributional analysis, and for disambiguating polysemy with a method that we refer to as semi-automatic uniqueness differentiation (SUDi). Uneek outputs the intersection and differences between their listed attributes, e.g. POS, dependencies, word forms, frame elements. This makes it an ideal supplement to methods for lumping or splitting in frame development processes. In order to make some of Uneek’s functions more clear, we employ SUDi on a small data set containing the polysemous verb "bake". As of now, Uneek may only run two files at a time, but there are plans to develop the tool so that it may simultaneously operate on multiple files. Finally, we relate the developmental plans for added functionality, to how such functions may support FrameNet work in the future.
|
|
| 10. |
- Megyesi, Beáta, 1971-, et al.
(författare)
-
Learner Corpus Anonymization in the Age of GDPR: Insights from the Creation of a Learner Corpus of Swedish
- 2018
-
Ingår i: Proceedings of the 7th Workshop on NLP for Computer Assisted Language Learning (NLP4CALL 2018) at SLTC, Stockholm, 7th November 2018 / edited by Ildikó Pilán, Elena Volodina, David Alfter and Lars Borin. - Linköpings universitet : Linköping University Electronic Press. - 1650-3686 .- 1650-3740. - 9789176851739
-
Konferensbidrag (refereegranskat)abstract
- This paper reports on the status of learner corpus anonymization for the ongoing research infrastructure project SweLL. The main project aim is to deliver and make available for research a well-annotated corpus of essays written by second language (L2) learners of Swedish. As the practice shows, annotation of learner texts is a sensitive process demanding a lot of compromises between ethical and legal demands on the one hand, and research and technical demands, on the other. Below, is a concise description of the current status of pseudonymization of language learner data to ensure anonymity of the learners, with numerous examples of the above-mentioned compromises.
|
|
