Publicaties
Gekozen filters:
Gekozen filters:
Unification, the answer to resemblance questions Universiteit Gent
Unification and integration: different yet the same? Universiteit Gent
ccording to the Oxford dictionary unification is ''the process of being united or made into a whole'', while integration is ''the action or process of integrating''. Integrating is further defined as ''combining (one thing) with another to form a whole''. Although there are different frameworks to describe how and to what extent unification could work (Kitcher 1981, 1989, Weber 1999, Schurz 1999, Mäki 2001), it seems as if unification and ...
Unifiers as Equivalences Proof-Relevant Unification of Dependently Typed Data Vrije Universiteit Brussel KU Leuven
Dependently typed languages such as Agda, Coq and Idris use a syntactic first-order unification algorithm to check definitions by dependent pattern matching. However, these algorithms don’t adequately consider the types of the terms being unified, leading to various unintended results. As a consequence, they require ad hoc restrictions to preserve soundness, but this makes them very hard to prove correct, modify, or extend. This paper proposes a ...
Lifting Proof-Relevant Unification to Higher Dimensions Vrije Universiteit Brussel KU Leuven
The role of unification in micro-explanations of physical laws Universiteit Gent
Causation, unification and the adequacy of explanations of facts Universiteit Gent
The role of unification in explanations of facts Universiteit Gent
In the literature on scientific explanation, there is a classical distinction between explanations of facts and explanations of laws. This paper is about explanations of facts. Our aim is to analyse the role of unification in explanations of this kind. We discuss five positions with respect to this role, argue for two of them and refute the three others.
Unification of Treatments and Interventions for Tinnitus Patients (UNITI): a study protocol for a multi-center randomized clinical trial KU Leuven
BACKGROUND: Tinnitus represents a relatively common condition in the global population accompanied by various comorbidities and severe burden in many cases. Nevertheless, there is currently no general treatment or cure, presumable due to the heterogeneity of tinnitus with its wide variety of etiologies and tinnitus phenotypes. Hence, most treatment studies merely demonstrated improvement in a subgroup of tinnitus patients. The majority of ...
Dependent Pattern Matching and Proof-Relevant Unification KU Leuven
Dependent type theory is a powerful language for writing functional programs with very precise types. It is used to write not only programs but also mathematical proofs that these programs satisfy certain properties. Because of this, languages based on dependent types – such as Coq, Agda, and Idris – are used both as programming languages and as interactive proof assistants. While dependent types give strong guarantees about your programs and ...