Refine
Year of publication
Document Type
- Working Paper (89)
- Article (14)
- Conference Proceeding (4)
- Book (1)
Has Fulltext
- yes (108)
Is part of the Bibliography
- no (108)
Keywords
- Lambda-Kalkül (17)
- Formale Semantik (9)
- Operationale Semantik (8)
- lambda calculus (8)
- Programmiersprache (7)
- concurrency (6)
- functional programming (6)
- Nebenläufigkeit (5)
- pi-calculus (5)
- semantics (5)
- Logik (4)
- Verifikation (4)
- adequate translations (4)
- contextual equivalence (4)
- letrec (4)
- automated deduction (3)
- call-by-need (3)
- context lemma (3)
- functional programming languages (3)
- observational semantics (3)
- Funktionale Programmiersprache (2)
- Funktionale Programmierung (2)
- Kontextuelle Gleichheit (2)
- Logics (2)
- Programmtransformation (2)
- Pufferspeicher (2)
- Semantics (2)
- Verification (2)
- call-by-name (2)
- context unification (2)
- infinitary lambda calculus (2)
- lambda-calculus (2)
- lazy evaluation (2)
- logics in artificial intelligence (2)
- non-determinism (2)
- nondeterminism (2)
- programming languages (2)
- rewriting (2)
- second order unification (2)
- unification (2)
- ADHD (1)
- Abstrakte Reduktion (1)
- Alice ML (1)
- Alltag (1)
- Baumgrammatiken (1)
- CVID (1)
- Call-by-Need (1)
- Clean (1)
- Contextual Equivalence (1)
- Corpus Inscriptionun Latinarum (1)
- Correctness (1)
- European Society for Immunodeficiencies (ESID) (1)
- Futures (1)
- German PID-NET registry (1)
- Haskell (1)
- IRSL (1)
- IgG substitution therapy (1)
- Kontextuelle Gleicheit (1)
- Lambda Calculus (1)
- Letrec-Kalkül (1)
- ML <Programmiersprache> (1)
- Nichtdeterminismus (1)
- Operational Semantics (1)
- PID prevalence (1)
- Pharmacodynamics (1)
- Polynomielles Wortproblem (1)
- Program Transformations (1)
- Programmkalküle (1)
- Programmkorrektheit (1)
- Römisches Reich (1)
- Sharing (1)
- Striktheitsanalyse (1)
- Target validation (1)
- Termination (1)
- Weilbach (1)
- Wortproblem (1)
- abstract reduction (1)
- adequate translation (1)
- aggression (1)
- bisimulation (1)
- call-by-need evaluation (1)
- call-by-need lambda calculus (1)
- chronostratigraphy (1)
- fMRI (1)
- fading (1)
- formal semantics (1)
- grammar-based compression (1)
- loess (1)
- luminescence dating (1)
- maternal care (1)
- nominal unification (1)
- parallel processes (1)
- polynomial word problem (1)
- precongruence (1)
- primary immunodeficiency (PID) (1)
- program correctness (1)
- programming calculi (1)
- randomized algorithms (1)
- registry for primary immunodeficiency (1)
- resilience (1)
- sharing (1)
- similarity (1)
- simulation (1)
- space improvements (1)
- space optimization (1)
- straight line programs (1)
- strictness analysis (1)
- translation (1)
- tree grammars (1)
- ventral striatum (1)
- verzögerte Auswertung (1)
Institute
- Informatik (96)
- Medizin (7)
- Georg-Speyer-Haus (2)
- Biochemie und Chemie (1)
- Geowissenschaften (1)
- Pharmazie (1)
- Physik (1)
- Zentrum für Biomolekulare Magnetische Resonanz (BMRZ) (1)
This paper proves several generic variants of context lemmas and thus contributes to improving the tools to develop observational semantics that is based on a reduction semantics for a language. The context lemmas are provided for may- as well as two variants of mustconvergence and a wide class of extended lambda calculi, which satisfy certain abstract conditions. The calculi must have a form of node sharing, e.g. plain beta reduction is not permitted. There are two variants, weakly sharing calculi, where the beta-reduction is only permitted for arguments that are variables, and strongly sharing calculi, which roughly correspond to call-by-need calculi, where beta-reduction is completely replaced by a sharing variant. The calculi must obey three abstract assumptions, which are in general easily recognizable given the syntax and the reduction rules. The generic context lemmas have as instances several context lemmas already proved in the literature for specific lambda calculi with sharing. The scope of the generic context lemmas comprises not only call-by-need calculi, but also call-by-value calculi with a form of built-in sharing. Investigations in other, new variants of extended lambda-calculi with sharing, where the language or the reduction rules and/or strategy varies, will be simplified by our result, since specific context lemmas are immediately derivable from the generic context lemma, provided our abstract conditions are met.
Reasoning about the correctness of program transformations requires a notion of program equivalence. We present an observational semantics for the concurrent lambda calculus with futures Lambda(fut), which formalizes the operational semantics of the programming language Alice ML. We show that natural program optimizations, as well as partial evaluation with respect to deterministic rules, are correct for Lambda(fut). This relies on a number of fundamental properties that we establish for our observational semantics.
We present a higher-order call-by-need lambda calculus enriched with constructors, case-expressions, recursive letrec-expressions, a seq-operator for sequential evaluation and a non-deterministic operator amb, which is locally bottom-avoiding. We use a small-step operational semantics in form of a normal order reduction. As equational theory we use contextual equivalence, i.e. terms are equal if plugged into an arbitrary program context their termination behaviour is the same. We use a combination of may- as well as must-convergence, which is appropriate for non-deterministic computations. We evolve different proof tools for proving correctness of program transformations. We provide a context lemma for may- as well as must- convergence which restricts the number of contexts that need to be examined for proving contextual equivalence. In combination with so-called complete sets of commuting and forking diagrams we show that all the deterministic reduction rules and also some additional transformations keep contextual equivalence. In contrast to other approaches our syntax as well as semantics does not make use of a heap for sharing expressions. Instead we represent these expressions explicitely via letrec-bindings.
Extending the method of Howe, we establish a large class of untyped higher-order calculi, in particular such with call-by-need evaluation, where similarity, also called applicative simulation, can be used as a proof tool for showing contextual preorder. The paper also demonstrates that Mann’s approach using an intermediate “approximation” calculus scales up well from a basic call-by-need non-deterministic lambdacalculus to more expressive lambda calculi. I.e., it is demonstrated, that after transferring the contextual preorder of a non-deterministic call-byneed lambda calculus to its corresponding approximation calculus, it is possible to apply Howe’s method to show that similarity is a precongruence. The transfer is not treated in this paper. The paper also proposes an optimization of the similarity-test by cutting off redundant computations. Our results also applies to deterministic or non-deterministic call-by-value lambda-calculi, and improves upon previous work insofar as it is proved that only closed values are required as arguments for similaritytesting instead of all closed expressions.
We develop a proof method to show that in a (deterministic) lambda calculus with letrec and equipped with contextual equivalence the call-by-name and the call-by-need evaluation are equivalent, and also that the unrestricted copy-operation is correct. Given a let-binding x = t, the copy-operation replaces an occurrence of the variable x by the expression t, regardless of the form of t. This gives an answer to unresolved problems in several papers, it adds a strong method to the tool set for reasoning about contextual equivalence in higher-order calculi with letrec, and it enables a class of transformations that can be used as optimizations. The method can be used in different kind of lambda calculi with cyclic sharing. Probably it can also be used in non-deterministic lambda calculi if the variable x is "deterministic", i.e., has no interference with non-deterministic executions. The main technical idea is to use a restricted variant of the infinitary lambda-calculus, whose objects are the expressions that are unrolled w.r.t. let, to define the infinite developments as a reduction calculus on the infinite trees and showing a standardization theorem.
Chronic granulomatous disease (CGD) is a primary immunodeficiency characterized by impaired antimicrobial activity in phagocytic cells. As a monogenic disease affecting the hematopoietic system, CGD is amenable to gene therapy. Indeed in a phase I/II clinical trial, we demonstrated a transient resolution of bacterial and fungal infections. However, the therapeutic benefit was compromised by the occurrence of clonal dominance and malignant transformation demanding alternative vectors with equal efficacy but safety-improved features. In this work we have developed and tested a self-inactivating (SIN) gammaretroviral vector (SINfes.gp91s) containing a codon-optimized transgene (gp91(phox)) under the transcriptional control of a myeloid promoter for the gene therapy of the X-linked form of CGD (X-CGD). Gene-corrected cells protected X-CGD mice from Aspergillus fumigatus challenge at low vector copy numbers. Moreover, the SINfes.gp91s vector generates substantial amounts of superoxide in human cells transplanted into immunodeficient mice. In vitro genotoxicity assays and longitudinal high-throughput integration site analysis in transplanted mice comprising primary and secondary animals for 11 months revealed a safe integration site profile with no signs of clonal dominance.
The bile acid activated transcription factor farnesoid X receptor (FXR) regulates numerous metabolic processes and is a rising target for the treatment of hepatic and metabolic disorders. FXR agonists have revealed efficacy in treating non-alcoholic steatohepatitis (NASH), diabetes and dyslipidemia. Here we characterize imatinib as first-in-class allosteric FXR modulator and report the development of an optimized descendant that markedly promotes agonist induced FXR activation in a reporter gene assay and FXR target gene expression in HepG2 cells. Differential effects of imatinib on agonist-induced bile salt export protein and small heterodimer partner expression suggest that allosteric FXR modulation could open a new avenue to gene-selective FXR modulators.
Gene-modified autologous hematopoietic stem cells (HSC) can provide ample clinical benefits to subjects suffering from X-linked chronic granulomatous disease (X-CGD), a rare inherited immunodeficiency characterized by recurrent, often life-threatening bacterial and fungal infections. Here we report on the molecular and cellular events observed in two young adults with X-CGD treated by gene therapy in 2004. After the initial resolution of bacterial and fungal infections, both subjects showed silencing of transgene expression due to methylation of the viral promoter, and myelodysplasia with monosomy 7 as a result of insertional activation of ecotropic viral integration site 1 (EVI1). One subject died from overwhelming sepsis 27 months after gene therapy, whereas a second subject underwent an allogeneic HSC transplantation. Our data show that forced overexpression of EVI1 in human cells disrupts normal centrosome duplication, linking EVI1 activation to the development of genomic instability, monosomy 7 and clonal progression toward myelodysplasia.