MC
M. Chiriţă
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
2 records found
1
Comprehension Category Type Theory (CCTT), introduced by Najmaei et al. (2026), is a type theory based on the structure of general comprehension categories. It represents morphisms between types directly in its syntax. These morphisms can act as coercions, and different morphisms between the same types remain distinguishable. CCTT therefore provides a built-in form of proof-relevant subtyping. In the general non-split theory, substitution preserves identities and composition only up to coherent isomorphisms. This makes conversion difficult to implement. This thesis studies the split theory, CCTTsplit, where substitution laws hold strictly and type morphisms remain part of the language. It presents an OCaml kernel for a selected fragment of this theory. This uses separate syntax for contexts, types, substitutions, and type morphisms. It represents ordinary terms as sections and uses normalization by evaluation to decide definitional equality. The implemented fragment includes explicit substitution, dependent products, dependent sums, identity types, functorial coercions for products and sums, and the basic action of identity-type coercions on reflexivity. The evaluation combines rule-based examples, regression tests, randomized property tests, mutation testing, and performance measurements. The kernel produces the expected result for all 31 curated cases. All 145 regression tests pass, and the suite detects all twelve deliberate faults. The randomized and performance experiments test conversion on larger inputs and reveal a remaining super-linear cost in type readback. These results show that the selected fragment can be implemented, but they do not prove soundness or completeness. The main limitations are incomplete checking of some substituted type morphisms, observational comparison of some higher-order coercions, missing identity-type coherence equations, and the lack of support for non-split CCTT.
...
Comprehension Category Type Theory (CCTT), introduced by Najmaei et al. (2026), is a type theory based on the structure of general comprehension categories. It represents morphisms between types directly in its syntax. These morphisms can act as coercions, and different morphisms between the same types remain distinguishable. CCTT therefore provides a built-in form of proof-relevant subtyping. In the general non-split theory, substitution preserves identities and composition only up to coherent isomorphisms. This makes conversion difficult to implement. This thesis studies the split theory, CCTTsplit, where substitution laws hold strictly and type morphisms remain part of the language. It presents an OCaml kernel for a selected fragment of this theory. This uses separate syntax for contexts, types, substitutions, and type morphisms. It represents ordinary terms as sections and uses normalization by evaluation to decide definitional equality. The implemented fragment includes explicit substitution, dependent products, dependent sums, identity types, functorial coercions for products and sums, and the basic action of identity-type coercions on reflexivity. The evaluation combines rule-based examples, regression tests, randomized property tests, mutation testing, and performance measurements. The kernel produces the expected result for all 31 curated cases. All 145 regression tests pass, and the suite detects all twelve deliberate faults. The randomized and performance experiments test conversion on larger inputs and reveal a remaining super-linear cost in type readback. These results show that the selected fragment can be implemented, but they do not prove soundness or completeness. The main limitations are incomplete checking of some substituted type morphisms, observational comparison of some higher-order coercions, missing identity-type coherence equations, and the lack of support for non-split CCTT.
Bachelor thesis
(2023)
-
M. Chiriţă, David M.J. Tax, Arman Naseri Jahfari, Ramin Ghorbani, Guohao Lan
The aim of this paper is to complete the gap in the knowledge and experiment using as little as only the heart rate of some subjects to manage to successfully authorise them in some supposed system. The focus will be on the Gaussian Mixture model and the One Class Support Vector Machine, both outlier detectors, because most of the past research was focused on supervised models. Using these two, this paper will experiment with recognising intruders with models trained to distinguish one authorised person and multiple authorised persons. In the first case, multiple data processing methods and hyperparameters will be tested together and compared. In the second case, the goal will be to use and modify the best-found parameters of the first case to train models that are able to detect multiple persons as authorised. This time, there are two methods that this paper is going to look into and compare their performance: training one single model to detect all the subjects and training multiple models, one per subject. The most notable results are with one authorised person, with a score of 0.936, with two authorised, 0.88, and with 12 authorised, 0.713, when using the area under the curve metric.
...
The aim of this paper is to complete the gap in the knowledge and experiment using as little as only the heart rate of some subjects to manage to successfully authorise them in some supposed system. The focus will be on the Gaussian Mixture model and the One Class Support Vector Machine, both outlier detectors, because most of the past research was focused on supervised models. Using these two, this paper will experiment with recognising intruders with models trained to distinguish one authorised person and multiple authorised persons. In the first case, multiple data processing methods and hyperparameters will be tested together and compared. In the second case, the goal will be to use and modify the best-found parameters of the first case to train models that are able to detect multiple persons as authorised. This time, there are two methods that this paper is going to look into and compare their performance: training one single model to detect all the subjects and training multiple models, one per subject. The most notable results are with one authorised person, with a score of 0.936, with two authorised, 0.88, and with 12 authorised, 0.713, when using the area under the curve metric.