Showing 1–6 of 6 results for author: Diehl, L

Deep Learning-Based Automatic Assessment of AgNOR-scores in Histopathology Images

Authors: Jonathan Ganz, Karoline Lipnik, Jonas Ammeling, Barbara Richter, Chloé Puget, Eda Parlak, Laura Diehl, Robert Klopfleisch, Taryn A. Donovan, Matti Kiupel, Christof A. Bertram, Katharina Breininger, Marc Aubreville

Abstract: Nucleolar organizer regions (NORs) are parts of the DNA that are involved in RNA transcription. Due to the silver affinity of associated proteins, argyrophilic NORs (AgNORs) can be visualized using silver-based staining. The average number of AgNORs per nucleus has been shown to be a prognostic factor for predicting the outcome of many tumors. Since manual detection of AgNORs is laborious, automat… ▽ More Nucleolar organizer regions (NORs) are parts of the DNA that are involved in RNA transcription. Due to the silver affinity of associated proteins, argyrophilic NORs (AgNORs) can be visualized using silver-based staining. The average number of AgNORs per nucleus has been shown to be a prognostic factor for predicting the outcome of many tumors. Since manual detection of AgNORs is laborious, automation is of high interest. We present a deep learning-based pipeline for automatically determining the AgNOR-score from histopathological sections. An additional annotation experiment was conducted with six pathologists to provide an independent performance evaluation of our approach. Across all raters and images, we found a mean squared error of 0.054 between the AgNOR- scores of the experts and those of the model, indicating that our approach offers performance comparable to humans. △ Less

Submitted 15 December, 2022; originally announced December 2022.

Comments: 6 pages, 2 figures, 1 table

Pan-tumor CAnine cuTaneous Cancer Histology (CATCH) dataset

Authors: Frauke Wilm, Marco Fragoso, Christian Marzahl, **gna Qiu, Chloé Puget, Laura Diehl, Christof A. Bertram, Robert Klopfleisch, Andreas Maier, Katharina Breininger, Marc Aubreville

Abstract: Due to morphological similarities, the differentiation of histologic sections of cutaneous tumors into individual subtypes can be challenging. Recently, deep learning-based approaches have proven their potential for supporting pathologists in this regard. However, many of these supervised algorithms require a large amount of annotated data for robust development. We present a publicly available da… ▽ More Due to morphological similarities, the differentiation of histologic sections of cutaneous tumors into individual subtypes can be challenging. Recently, deep learning-based approaches have proven their potential for supporting pathologists in this regard. However, many of these supervised algorithms require a large amount of annotated data for robust development. We present a publicly available dataset of 350 whole slide images of seven different canine cutaneous tumors complemented by 12,424 polygon annotations for 13 histologic classes, including seven cutaneous tumor subtypes. In inter-rater experiments, we show a high consistency of the provided labels, especially for tumor annotations. We further validate the dataset by training a deep neural network for the task of tissue segmentation and tumor subtype classification. We achieve a class-averaged Jaccard coefficient of 0.7047, and 0.9044 for tumor in particular. For classification, we achieve a slide-level accuracy of 0.9857. Since canine cutaneous tumors possess various histologic homologies to human tumors the added value of this dataset is not limited to veterinary pathology but extends to more general fields of application. △ Less

Submitted 26 August, 2022; v1 submitted 27 January, 2022; originally announced January 2022.

Comments: Submitted to Scientific Data. 15 pages, 9 figures, 6 tables

Report number: 588

Journal ref: Scientific Data vol. 9 (2022)

Efficient lambda encodings for Mendler-style coinductive types in Cedille

Authors: Christopher Jenkins, Aaron Stump, Larry Diehl

Abstract: In the calculus of dependent lambda eliminations (CDLE), it is possible to define inductive datatypes via lambda encodings that feature constant-time destructors and a course-of-values induction scheme. This paper begins to address the missing derivations for the dual, coinductive types. Our derivation utilizes new methods within CDLE, as there are seemingly fundamental difficulties in adapting pr… ▽ More In the calculus of dependent lambda eliminations (CDLE), it is possible to define inductive datatypes via lambda encodings that feature constant-time destructors and a course-of-values induction scheme. This paper begins to address the missing derivations for the dual, coinductive types. Our derivation utilizes new methods within CDLE, as there are seemingly fundamental difficulties in adapting previous known approaches for deriving inductive types. The lambda encodings we present implementing coinductive types feature constant-time constructors and a course-of-values corecursion scheme. Coinductive type families are also supported, enabling proofs for many standard coinductive properties such as stream bisimulation. All work is mechanically verified by the Cedille tool, an implementation of CDLE. △ Less

Submitted 30 April, 2020; originally announced May 2020.

Comments: In Proceedings MSFP 2020, arXiv:2004.14735

Journal ref: EPTCS 317, 2020, pp. 72-97

Course-of-Value Induction in Cedille

Authors: Denis Firsov, Larry Diehl, Christopher Jenkins, Aaron Stump

Abstract: In the categorical setting, histomorphisms model a course-of-value recursion scheme that allows functions to be defined using arbitrary previously computed values. In this paper, we use the Calculus of Dependent Lambda Eliminations (CDLE) to derive a lambda-encoding of inductive datatypes that admits course-of-value induction. Similar to course-of-value recursion, course-of-value induction gives a… ▽ More In the categorical setting, histomorphisms model a course-of-value recursion scheme that allows functions to be defined using arbitrary previously computed values. In this paper, we use the Calculus of Dependent Lambda Eliminations (CDLE) to derive a lambda-encoding of inductive datatypes that admits course-of-value induction. Similar to course-of-value recursion, course-of-value induction gives access to inductive hypotheses at arbitrary depth of the inductive arguments of a function. We show that the derived course-of-value datatypes are well-behaved by proving Lambek's lemma and characterizing the computational behavior of the induction principle. Our work is formalized in the Cedille programming language and also includes several examples of course-of-value functions. △ Less

Submitted 7 March, 2019; v1 submitted 28 November, 2018; originally announced November 2018.

Generic Zero-Cost Reuse for Dependent Types

Authors: Larry Diehl, Denis Firsov, Aaron Stump

Abstract: Dependently typed languages are well known for having a problem with code reuse. Traditional non-indexed algebraic datatypes (e.g. lists) appear alongside a plethora of indexed variations (e.g. vectors). Functions are often rewritten for both non-indexed and indexed versions of essentially the same datatype, which is a source of code duplication. We work in a Curry-style dependent type theory, w… ▽ More Dependently typed languages are well known for having a problem with code reuse. Traditional non-indexed algebraic datatypes (e.g. lists) appear alongside a plethora of indexed variations (e.g. vectors). Functions are often rewritten for both non-indexed and indexed versions of essentially the same datatype, which is a source of code duplication. We work in a Curry-style dependent type theory, where the same untyped term may be classified as both the non-indexed and indexed versions of a datatype. Many solutions have been proposed for the problem of dependently typed reuse, but we exploit Curry-style type theory in our solution to not only reuse data and programs, but do so at zero-cost (without a runtime penalty). Our work is an exercise in dependently typed generic programming, and internalizes the process of zero-cost reuse as the identity function in a Curry-style theory. △ Less

Submitted 9 July, 2018; v1 submitted 21 March, 2018; originally announced March 2018.

Comments: Additional section on Generic Relational Reuse

Zero-Cost Coercions for Program and Proof Reuse

Authors: Larry Diehl, Aaron Stump

Abstract: We introduce the notion of identity coercions between non-indexed and indexed variants of inductive datatypes, such as lists and vectors. An identity coercion translates one type to another such that the coercion function definitionally reduces to the identity function. This allows us to reuse vector programs to derive list programs (and vice versa), without any runtime cost. This also allows us t… ▽ More We introduce the notion of identity coercions between non-indexed and indexed variants of inductive datatypes, such as lists and vectors. An identity coercion translates one type to another such that the coercion function definitionally reduces to the identity function. This allows us to reuse vector programs to derive list programs (and vice versa), without any runtime cost. This also allows us to reuse vector proofs to derive list proofs (and vice versa), without the cost of equational reasoning proof obligations. Our work is formalized in Cedille, a dependently typed programming language based on a type-annotated Curry-style type the- ory with implicit (or, erased) products (or, dependent functions), and relies crucially on erasure to introduce definitional equalities between underlying untyped terms. △ Less

Submitted 2 February, 2018; originally announced February 2018.