| 1. |
- Abel, Andreas, 1974, et al.
(författare)
-
A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized
- 2023
-
Ingår i: Proceedings of the ACM on Programming Languages. - 2475-1421. ; 7:ICFP, s. 920-954
-
Tidskriftsartikel (refereegranskat)abstract
- We present a graded modal type theory, a dependent type theory with grades that can be used to enforce various properties of the code. The theory has Pi-types, weak and strong Sigma-types, natural numbers, an empty type, and a universe, and we also extend the theory with a unit type and graded Sigma-types. The theory is parameterized by a modality, a kind of partially ordered semiring, whose elements (grades) are used to track the usage of variables in terms and types. Different modalities are possible. We focus mainly on quantitative properties, in particular erasure: with the erasure modality one can mark function arguments as erasable. The theory is fully formalized in Agda. The formalization, which uses a syntactic Kripke logical relation at its core and is based on earlier work, establishes major meta-theoretic properties such as subject reduction, consistency, normalization, and decidability of definitional equality. We also prove a substitution theorem for grade assignment, and preservation of grades under reduction. Furthermore we study an extraction function that translates terms to an untyped λ-calculus and removes erasable content, in particular function arguments with the "erasable"grade. For a certain class of modalities we prove that extraction is sound, in the sense that programs of natural number type have the same value before and after extraction. Soundness of extraction holds also for open programs, as long as all variables in the context are erasable, the context is consistent, and erased matches are not allowed for weak Sigma-types.
|
|
| 2. |
- Capriotti, Paolo, et al.
(författare)
-
Higher Lenses
- 2021
-
Ingår i: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS).
-
Konferensbidrag (refereegranskat)
|
|
| 3. |
- Danielsson, Nils Anders, 1979
(författare)
-
Higher Inductive Type Eliminators Without Paths
- 2020
-
Ingår i: 25th International Conference on Types for Proofs and Programs. - Saarbrücken/Wadern, Germany : Schloss Dagstuhl – Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing. - 1868-8969. - 9783959771580
-
Konferensbidrag (refereegranskat)
|
|
| 4. |
- López Juan, Víctor, 1992, et al.
(författare)
-
Practical dependent type checking using twin types
- 2020
-
Ingår i: TyDe 2020 - Proceedings of the 5th ACM SIGPLAN International Workshop on Type-Driven Development, co-located with ICFP 2020. - New York, NY, USA : ACM. ; , s. 11-23
-
Konferensbidrag (refereegranskat)abstract
- People writing proofs or programs in dependently typed languages can omit some function arguments in order to decrease the code size and improve readability. Type checking such a program involves filling in each of these implicit arguments in a type-correct way. This is typically done using some form of unification. One approach to unification, taken by Agda, involves sometimes starting to unify terms before their types are known to be equal: in some cases one can make progress on unifying the terms, and then use information gleaned in this way to unify the types. This flexibility allows Agda to solve implicit arguments that are not found by several other systems. However, Agda's implementation is buggy: sometimes the solutions chosen are ill-typed, which can cause the type checker to crash. With Gundry and McBride's twin variable technique one can also start to unify terms before their types are known to be equal, and furthermore this technique is accompanied by correctness proofs. However, so far this technique has not been tested in practice as part of a full type checker. We have reformulated Gundry and McBride's technique without twin variables, using only twin types, with the aim of making the technique easier to implement in existing type checkers (in particular Agda). We have also introduced a type-agnostic syntactic equality rule that seems to be useful in practice. The reformulated technique has been tested in a type checker for a tiny variant of Agda. This type checker handles at least one example that Coq, Idris, Lean and Matita cannot handle, and does so in time and space comparable to that used by Agda. This suggests that the reformulated technique is usable in practice.
|
|
| 5. |
|
|
| 6. |
- Altenkirch, Thorsten, et al.
(författare)
-
Type Theory with Weak J
- 2017
-
Ingår i: 23rd International Conference on Types for Proofs and Programs, TYPES 2017, Budapest, Hungary, 29 May - 1 June 2017, Abstracts. - Budapest, Hungary : Department of Programming Languages and Compilers, Faculty of Informatics, Eötvös Loránd University. - 9789632848839
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)
|
|
| 7. |
- Danielsson, Nils Anders, 1979, et al.
(författare)
-
Towards practical out-of-order unification
- 2017
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - Budapest, Hungary : Department of Programming Languages and Compilers, Faculty of Informatics, Eötvös Loránd University. - 1868-8969. ; 104, s. 49-50
-
Konferensbidrag (refereegranskat)
|
|
| 8. |
- Geidenstam, Nina, et al.
(författare)
-
Amino Acid Signatures to Evaluate the Beneficial Effects of Weight Loss
- 2017
-
Ingår i: International Journal of Endocrinology. - : Hindawi Limited. - 1687-8337 .- 1687-8345. ; 2017
-
Tidskriftsartikel (refereegranskat)abstract
- Aims. We investigated the relationship between circulating amino acid levels and obesity; to what extent weight loss followed by weight maintenance can correct amino acid abnormalities; and whether amino acids are related to weight loss. Methods. Amino acids associated with waist circumference (WC) and BMI were studied in 804 participants from the Malmö Diet and Cancer Cardiovascular Cohort (MDC-CC). Changes in amino acid levels were analyzed after weight loss and weight maintenance in 12 obese subjects and evaluated in a replication cohort (n = 83). Results. Out of the eight identified BMI-associated amino acids from the MDC-CC, alanine, isoleucine, tyrosine, phenylalanine, and glutamate decreased after weight loss, while asparagine increased after weight maintenance. These changes were validated in the replication cohort. Scores that were constructed based on obesity-associated amino acids and known risk factors decreased in the ≥10% weight loss group with an associated change in BMI (R(2) = 0.16-0.22, p < 0.002), whereas the scores increased in the <10% weight loss group (p < 0.0004). Conclusions. Weight loss followed by weight maintenance leads to differential changes in amino acid levels associated with obesity. Treatment modifiable scores based on epidemiological and interventional data may be used to evaluate the potential metabolic benefit of weight loss.
|
|
| 9. |
- Altenkirch, Thorsten, et al.
(författare)
-
Partiality, Revisited
- 2016
-
Ingår i: TYPES 2016, Types for Proofs and Programs, 22nd Meeting, Novi Sad, Serbia, 23 – 26 May, 2016, Book of Abstracts.
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)
|
|
| 10. |
- Danielsson, Anders, et al.
(författare)
-
Svåra samtal med patienter tränas på kurs med skådespelare : En medveten strategi hjälper både läkare och patient
- 2016
-
Ingår i: Läkartidningen. - 0023-7205. ; 113:47
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- The physician’s communication skill influences the patient’s mental and physical wellbeing, as well as the physician’s own experience of stress. Most patients wish to be informed about their disease, by physicians who are honest, gives time, sustains hope, listens and shows compassion and empathy. Even though there are established guidelines on how to break bad news, the physician must find out and respond to the unique reactions and needs of each individual, in order to communicate successfully. There is no consensus on how to construct and evaluate communication skills training programs for physicians, and more RCT-studies are requested.
|
|
