| 31. |
- Abel, Andreas, 1974, et al.
(författare)
-
Normalization by Evaluation for Martin-Löf Type Theory with Equality Judgements
- 2007
-
Ingår i: Proceedings of 22nd IEEE Annual Symposium on Logic in ComputerScience, Wroclaw, Poland, July 2007.. - : IEEE. - 1043-6871. - 0769529089 ; , s. 3-12
-
Tidskriftsartikel (refereegranskat)abstract
- The decidability of equality is proved for Martin-Löf type theory with a universe a la Russell and typed beta-eta-equality judgements. A corollary of this result is that the constructor for dependent function types is injective, a property which is crucial for establishing the correctness of the type-checking algorithm. The decision procedure uses normalization by evaluation, an algorithm which first interprets terms in a domain with untyped semantic elements and then extracts normal forms. The correctness of this algorithm is established using a PER-model and a logical relation between syntax and semantics.
|
|
| 32. |
- Abel, Andreas, 1974, et al.
(författare)
-
Normalization by evaluation for sized dependent types
- 2017
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 1:ICFP, s. 33:1-33:30
-
Tidskriftsartikel (refereegranskat)abstract
- Sized types have been developed to make termination checking more perspicuous, more powerful, and more modular by integrating termination into type checking. In dependently-typed proof assistants where proofs by induction are just recursive functional programs, the termination checker is an integral component of the trusted core, as validity of proofs depend on termination. However, a rigorous integration of full-fledged sized types into dependent type theory is lacking so far. Such an integration is non-trivial, as explicit sizes in proof terms might get in the way of equality checking, making terms appear distinct that should have the same semantics. In this article, we integrate dependent types and sized types with higher-rank size polymorphism, which is essential for generic programming and abstraction. We introduce a size quantifier (\forall) which lets us ignore sizes in terms for equality checking, alongside with a second quantifier Î for abstracting over sizes that do affect the semantics of types and terms. Judgmental equality is decided by an adaptation of normalization-by-evaluation for our new type theory, which features type shape-directed reflection and reification. It follows that subtyping and type checking of normal forms are decidable as well, the latter by a bidirectional algorithm.
|
|
| 33. |
|
|
| 34. |
- Abel, Andreas, 1974, et al.
(författare)
-
Untyped algorithmic equality for Martin-Löf's logical framework with surjective pairs
- 2007
-
Ingår i: Fundamenta Informaticae. - 0169-2968. ; 77:4, s. 345-395
-
Tidskriftsartikel (refereegranskat)abstract
- Martin-Löf's Logical Framework is extended by strong Sigma-types and presented via judgmental equality with rules for extensionality and surjective pairing. Soundness of the framework rules is proven via a generic PER model on untyped terms. An algorithmic version of the framework is given through an untyped beta eta-equality test and a bidirectional type checking algorithm. Completeness is proven by instantiating the PER model with eta-equality on beta-normal forms, which is shown equivalent to the algorithmic equality.
|
|
| 35. |
- Abel, Andreas, 1974, et al.
(författare)
-
Well-founded recursion with copatterns and sized types
- 2016
-
Ingår i: Journal of Functional Programming. - : Cambridge University Press (CUP). - 0956-7968 .- 1469-7653. ; 26
-
Tidskriftsartikel (refereegranskat)abstract
- In this paper, we study strong normalization of a core language based on System F-omega which supports programming with finite and infinite structures. Finite data such as finite lists and trees is defined via constructors and manipulated via pattern matching, while infinite data such as streams and infinite trees is defined by observations and synthesized via copattern matching. Taking a type-based approach to strong normalization, we track size information about finite and infinite data in the type. We exploit the duality of pattern and copatterns to give a unifying semantic framework which allows us to elegantly and uniformly support both well-founded induction and coinduction by rewriting. The strong normalization proof is structured around Girard's reducibility candidates. As such, our system allows for non determinism and does not rely on coverage. Since System F-omega is general enough that it can be the target of compilation for the Calculus of Constructions, this work is a significant step towards representing observation-based infinite data in proof assistants such as Coq and Agda.
|
|
| 36. |
- Abel, Frida, 1974, et al.
(författare)
-
A 6-gene signature identifies four molecular subgroups of neuroblastoma
- 2011
-
Ingår i: Cancer Cell International. - : Springer Science and Business Media LLC. - 1475-2867. ; 11:9
-
Tidskriftsartikel (refereegranskat)abstract
- Abstract Background There are currently three postulated genomic subtypes of the childhood tumour neuroblastoma (NB); Type 1, Type 2A, and Type 2B. The most aggressive forms of NB are characterized by amplification of the oncogene MYCN (MNA) and low expression of the favourable marker NTRK1. Recently, mutations or high expression of the familial predisposition gene Anaplastic Lymphoma Kinase (ALK) was associated to unfavourable biology of sporadic NB. Also, various other genes have been linked to NB pathogenesis. Results The present study explores subgroup discrimination by gene expression profiling using three published microarray studies on NB (47 samples). Four distinct clusters were identified by Principal Components Analysis (PCA) in two separate data sets, which could be verified by an unsupervised hierarchical clustering in a third independent data set (101 NB samples) using a set of 74 discriminative genes. The expression signature of six NB-associated genes ALK, BIRC5, CCND1, MYCN, NTRK1, and PHOX2B, significantly discriminated the four clusters (p
|
|
| 37. |
- Abel, Frida, 1974, et al.
(författare)
-
Analyses of apoptotic regulators CASP9 and DFFA at 1P36.2, reveal rare allele variants in human neuroblastoma tumours.
- 2002
-
Ingår i: British journal of cancer. - : Springer Science and Business Media LLC. - 0007-0920 .- 1532-1827. ; 86:4, s. 596-604
-
Tidskriftsartikel (refereegranskat)abstract
- The genes encoding Caspase-9 and DFF45 have both recently been mapped to chromosome region 1p36.2, that is a region alleged to involve one or several tumour suppressor genes in neuroblastoma tumours. This study presents an update contig of the 'Smallest Region of Overlap of deletions' in Scandinavian neuroblastoma tumours and suggests that DFF45 is localized in the region. The genomic organization of the human DFF45 gene, deduced by in-silico comparisons of DNA sequences, is described for the first time in this paper. In the present study 44 primary tumours were screened for mutation by analysis of the genomic sequences of the genes. In two out of the 44 tumours this detected in the DFFA gene one rare allele variant that caused a non-polar to a polar amino acid exchange in a preserved hydrophobic patch of DFF45. One case was hemizygous due to deletion of the more common allele of this polymorphism. Out of 194 normal control alleles only one was found to carry this variant allele, so in respect of it, no healthy control individual out of 97 was homozygous. Moreover, our RT-PCR expression studies showed that DFF45 is preferably expressed in low-stage neuroblastoma tumours and to a lesser degree in high-stage neuroblastomas. We conclude that although coding mutations of Caspase-9 and DFF45 are infrequent in neuroblastoma tumours, our discovery of a rare allele in two neuroblastoma cases should be taken to warrant further studies of the role of DFF45 in neuroblastoma genetics.
|
|
| 38. |
- Abel, Frida, 1974, et al.
(författare)
-
Gain of chromosome arm 17q is associated with unfavourable prognosis in neuroblastoma, but does not involve mutations in the somatostatin receptor 2(SSTR2) gene at 17q24.
- 1999
-
Ingår i: British journal of cancer. - : Springer Science and Business Media LLC. - 0007-0920 .- 1532-1827. ; 81:8, s. 1402-9
-
Tidskriftsartikel (refereegranskat)abstract
- Deletion of chromosome arm 1p and amplification of the MYCN oncogene are well-recognized genetic alterations in neuroblastoma cells. Recently, another alteration has been reported; gain of the distal part of chromosome arm 17q. In this study 48 neuroblastoma tumours were successfully analysed for 17q status in relation to known genetic alterations. Chromosome 17 status was detected by fluorescence in situ hybridization (FISH). Thirty-one of the 48 neuroblastomas (65%) showed 17q gain, and this was significantly associated with poor prognosis. As previously reported, 17q gain was significantly associated with metastatic stage 4 neuroblastoma and more frequently detected than both deletion of chromosome arm 1p and MYCN amplification in tumours of all stages. 17q gain also showed a strong correlation to survival probability (P = 0.0009). However, the most significant correlation between 17q gain and survival probability was observed in children with low-stage tumours (stage 1, 2, 3 and 4S), with a survival probability of 100% at 5 years from diagnosis for children with tumours showing no 17q gain compared to 52.5% for those showing 17q gain (P = 0.0021). This suggests that 17q gain as a prognostic factor plays a more crucial role in low-stage tumours. Expression of the somatostatin receptor 2 (SSTR2), localized in chromosome region 17q24, has in previous studies been shown to be positively related to survival in neuroblastoma. A point mutation in the SSTR2 gene has earlier been reported in a human small-cell lung cancer. In this study, mutation screening of the SSTR2 gene in 43 neuroblastoma tumours was carried out with polymerase chain reaction-based single-stranded conformation polymorphism/heteroduplex (SSCP/HD) and DNA sequencing, and none of the tumours showed any aberrations in the SSTR2 gene. These data suggest that mutations in the SSTR2 gene are uncommon in neuroblastoma tumours and do not correlate with either the 17q gain often seen or the reason some tumours do not express SSTR2 receptors. Overall, this study indicates that gain of chromosome arm 17q is the most frequently occurring genetic alteration, and that it is associated with established prognostic factors.
|
|
| 39. |
- Abel, Frida, 1974
(författare)
-
Genetic studies of neuroblastoma with emphasis on the apoptotic pathway
- 2004
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Aim: The objective of this thesis was to find genes and chromosomal regions involved in neuroblastoma (NB) tumor progression. NB is a childhood tumor of the sympathetic nervous system that generally occurs spontaneously. Biologically, NB has a complex heterogeneity from tumor progression to tumor regression, dependent on clinical stage and age at diagnosis. The main genetic markers, which are also of prognostic value in NB, are amplification of the oncogene MYCN, deletion of chromosome arm 1p and gain of chromosome arm 17q. Results: We have been shown using fluorescence in situ hybridization (FISH) on a Scandinavian tumor material, that 17q gain is present in approximately 65% of all NB stages, is significantly associated with poor prognosis and predicts survival. The gene encoding somatostatin receptor 2 (SSTR2), localized in chromosome region 17q24, was not found to be mutated in any NB, when analyzed with PCR-based single stranded conformation polymorphism/heteroduplex (SSCP/HD) and DNA sequencing. In a tentative effort of defining of the location of a general embryonal tumor suppressor gene (TSG) on 1p, we combined the smallest region of overlap (SRO) of 1p deletions in NB tumors and germ cell tumors (GCTs). We thus delimited the NB/GCT SRO to approximately 5 cM between markers D1S508 and D1S244, and fine-mapped this region by radiation hybrid mapping and construction of a bacterial artificial chromosome (BAC) contig. A homozygously deleted region in an NB cell line was found to partially overlap the proximal part of the 5 cM-SRO defined by us, which further focused our search for a TSG to a 500 kb candidate region in 1p36.22. Two attractive candidate NB TSGs, DFFA and CASP9, are both located in 1p36.2 and encode key apoptotic mediators. In fact, DFFA resides in the 500 kb TSG candidate region. Via sequence analysis of the entire tumor material, we found three different coding alterations in DFFA which all affect the highly conserved N-terminal regulatory domain of DFF45. Using RT-PCR and real-time RT-PCR (TaqMan) studies, we were able to show that both DFFA and CASP9 are preferably expressed in NB tumors with favorable outcome. It has been proposed that lack of apoptosis plays an important role in tumor progression. We therefore screened an array with cDNAs involved in the apoptotic process, to find genes differentially expressed in NB tumors with unfavorable versus favorable biology. Using real-time RT-PCR analysis, we verified the differential expression of several transcripts encoding mitochondrial apoptotic mediators. Conclusions: We have shown that 17q gain is the most frequently detected alteration in NB and that it is associated with established prognostic factors. We narrowed down the TSG candidate region on 1p and found mutations in a gene localized in the region possessing fundamental functions in apoptosis. Our results also suggest that the mitochondrial apoptotic pathway is suppressed at multiple steps in advanced stages of NB tumors, due to imbalance between anti-apoptotic and pro-apoptotic mediators.
|
|
| 40. |
- Abel, Frida, 1974, et al.
(författare)
-
Imbalance of the mitochondrial pro- and anti-apoptotic mediators in neuroblastoma tumours with unfavourable biology.
- 2005
-
Ingår i: European journal of cancer (Oxford, England : 1990). - : Elsevier BV. - 0959-8049. ; 41:4, s. 635-46
-
Tidskriftsartikel (refereegranskat)abstract
- It has been proposed that a lack of apoptosis plays an important role in neuroblastoma (NB) progression. We therefore screened cDNA array filters, including 198 apoptotic genes, in order to identify mRNA transcripts that are differentially expressed in tumours with unfavourable versus favourable biology. Twenty-one genes were analysed further using real-time reverse-transcriptase-polymerase chain reaction (RT-PCR). Significantly lower levels of DNCL1 (PIN; P(c)(corrected) = 0.0054) and NTRK1 (TrkA; P(c) = 0.039) were found in NB tumours with unfavourable biology. In addition, BID, BCL2, APAF1, CASP2, CASP3 and CASP9 were found to be preferentially expressed in tumours with favourable biology, whereas CDKN1A (p21), IL2RA, and MCL1, were found to be preferentially expressed in NB tumours with unfavourable biology. In conclusion, mRNA levels of transcripts encoding pro-apoptotic mediators of the mitochondrial apoptotic pathway were found to be expressed to a lower extent in tumours with unfavourable biology. Our data also suggest that the mitochondrial pathway is suppressed in advanced stages of NB tumours, due to an imbalance between anti-apoptotic and pro-apoptotic mediators which is a finding that may have therapeutic significance.
|
|
