المؤلفون: Cohen, Cyril, Crance, Enzo, Mahboubi, Assia

المساهمون: Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Mitsubishi Electric R&D Centre Europe France (MERCE-France), Mitsubishi Electric France, Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N), Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-NANTES UNIVERSITÉ - École Centrale de Nantes (Nantes Univ - ECN), Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes université - UFR des Sciences et des Techniques (Nantes univ - UFR ST), Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Nantes Université (Nantes Univ), Laboratoire des Sciences du Numérique de Nantes (LS2N), Stéphanie Weirich, European Project: 101001995,FRESCO(2021)

المصدر: Lecture Notes in Computer Science ; ESOP 2024 - 33rd European Symposium on Programming ; https://hal.science/hal-04177913 ; ESOP 2024 - 33rd European Symposium on Programming, Apr 2024, Luxembourg, Luxembourg. pp.239-268

مصطلحات موضوعية: Parametricity, Representation independence, Univalence, Proof assistants, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]

جغرافية الموضوع: Luxembourg

Relation: info:eu-repo/grantAgreement//101001995/EU/Fast and Reliable Symbolic Computation/FRESCO

الاتاحة: https://hal.science/hal-04177913
https://hal.science/hal-04177913v5/document
https://hal.science/hal-04177913v5/file/main.pdf

المؤلفون: Coquand, Thierry, 1961, Ruch, Fabian, 1989, Sattler, Christian, 1988

المصدر: Bevisteori och semantik för homotopitypteori i högre ordningens kategorier Mathematical Structures in Computer Science. 31(9):979-1002

مصطلحات موضوعية: Dependent type theory, constructive models of univalence, left-exact modalities, homotopy type theory, sheaf models

وصف الملف: electronic

URL الوصول: https://research.chalmers.se/publication/527439
https://research.chalmers.se/publication/527439/file/527439_Fulltext.pdf

المؤلفون: Altenkirch, Thorsten, Boulier, Simon, Kaposi, Ambrus, Sattler, Christian, 1988, Sestini, Filippo

المصدر: 24th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2021 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Virtual, Online Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 12650:1-21

مصطلحات موضوعية: Univalence, Induction-recursion, Setoid model, Induction-induction, Type theory, Function extensionality

وصف الملف: electronic

URL الوصول: https://research.chalmers.se/publication/524826
https://research.chalmers.se/publication/524826/file/524826_Fulltext.pdf

المؤلفون: Wullaert, Kobe, Matthes, Ralph, Ahrens, Benedikt

المساهمون: Kobe Wullaert and Ralph Matthes and Benedikt Ahrens

مصطلحات موضوعية: Univalence, Monoidal categories, Rezk completion, Displayed (bi)categories, Proof assistant Coq, UniMath library

وصف الملف: application/pdf

Relation: Is Part Of LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022); https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.15

الاتاحة: https://doi.org/10.4230/LIPIcs.TYPES.2022.15
https://nbn-resolving.org/urn:nbn:de:0030-drops-184580
https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.15

المؤلفون: Orton, Richard Ian

المساهمون: Pitts, Andrew Mawdesley

مصطلحات موضوعية: 004.01, type theory, homtopy type theory, univalent type theory, univalence, cubical type theory, cubical sets, HoTT, UTT, internal language, topos

URL الوصول: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.767769

المؤلفون: Sercan Kazımoğlu, Erhan Deniz, Luminita-Ioana Cotirla

المصدر: Axioms; Volume 12; Issue 6; Pages: 563

مصطلحات موضوعية: analytic functions, Miller–Ross functions, univalence, convexity, special functions, univalent functions, integral operators

وصف الملف: application/pdf

Relation: Mathematical Analysis; https://dx.doi.org/10.3390/axioms12060563

الاتاحة: https://doi.org/10.3390/axioms12060563

المؤلفون: Coquand, Thierry, 1961, Huber, Simon, 1984, Sattler, Christian, 1988

المصدر: Bevisteori och semantik för homotopitypteori i högre ordningens kategorier Logical Methods in Computer Science. 18(1)

مصطلحات موضوعية: univalence, sconing, cubical type theory, canonicity, Artin glueing

وصف الملف: electronic

URL الوصول: https://research.chalmers.se/publication/528701
https://research.chalmers.se/publication/528701/file/528701_Fulltext.pdf

المؤلفون: Ji Hyang Park, Hari Mohan Srivastava, Nak Eun Cho

المصدر: AIMS Mathematics, Vol 6, Iss 10, Pp 11380-11402 (2021)

مصطلحات موضوعية: analytic functions, univalent functions, integral operators, special functions, lommel functions, univalence, convexity, quantum (or q-) calculus, Mathematics, QA1-939

وصف الملف: electronic resource

Relation: https://doaj.org/toc/2473-6988

URL الوصول: https://doaj.org/article/e1038ef852234dce8af39868ff4aecc0

المؤلفون: Cohen, Cyril, Crance, Enzo, Mahboubi, Assia

المساهمون: Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Mitsubishi Electric R&D Centre Europe France (MERCE-France), Mitsubishi Electric France, Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N), Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-École Centrale de Nantes (Nantes Univ - ECN), Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes université - UFR des Sciences et des Techniques (Nantes univ - UFR ST), Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Nantes Université (Nantes Univ), European Project: 101001995,FRESCO(2021)

المصدر: https://hal.science/hal-04177913 ; 2023.

مصطلحات موضوعية: Parametricity, Representation independence, Univalence, Proof assistants, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]

Relation: info:eu-repo/grantAgreement//101001995/EU/Fast and Reliable Symbolic Computation/FRESCO; hal-04177913; https://hal.science/hal-04177913; https://hal.science/hal-04177913v3/document; https://hal.science/hal-04177913v3/file/main%20%281%29.pdf

الاتاحة: https://hal.science/hal-04177913
https://hal.science/hal-04177913v3/document
https://hal.science/hal-04177913v3/file/main%20%281%29.pdf

المؤلفون: Elif Yaşar

المصدر: Journal of Taibah University for Science, Vol 15, Iss 1, Pp 71-76 (2021)

مصطلحات موضوعية: harmonic mapping, convolution, univalence, Science (General), Q1-390

وصف الملف: electronic resource

Relation: https://doaj.org/toc/1658-3655

URL الوصول: https://doaj.org/article/7a4407fbfe7d44ada62d25d04c49f310

المؤلفون: Mohsan Raza, Sarfraz Nawaz Malik, Qin Xin, Muhey U. Din, Luminiţa-Ioana Cotîrlă

المصدر: Mathematics; Volume 10; Issue 9; Pages: 1361

مصطلحات موضوعية: Bessel functions, modified Bessel functions, spherical Bessel functions, integral operators, Kudriasov conditions, univalence criteria

وصف الملف: application/pdf

Relation: https://dx.doi.org/10.3390/math10091361

الاتاحة: https://doi.org/10.3390/math10091361

المؤلفون: Angiuli, Carlo, Cavallo, Evan, Mörtberg, Anders, Zeuner, Max

المصدر: Proceedings of the ACM on Programming Languages. 5(POPL)

مصطلحات موضوعية: Representation Independence, Univalence, Higher Inductive Types, Proof Assistants, Cubical Type Theory

وصف الملف: print

URL الوصول: https://urn.kb.se/resolve?urn=urn:nbn:se:su:diva-196801
https://doi.org/10.1145/3434293

المؤلفون: Chuaqui, M, Osgood, B

مصطلحات موضوعية: UNIVALENCE CRITERION, NEHARI, EXTENSIONS, THEOREM, DISK

وصف الملف: 19 páginas; application/pdf

Relation: https://repositorio.uc.cl/handle/11534/76017; WOS:000080328700004

الاتاحة: https://repositorio.uc.cl/handle/11534/76017

المؤلفون: Chuaqui, Martin, Duren, Peter, Osgood, Brad

مصطلحات موضوعية: Convex mapping, Schwarzian derivative, Schwarzian norm, univalence, Schwarz lemma, Schwarz-Christoffel formula, quasidisk, John domain

وصف الملف: 12 páginas; application/pdf

Relation: https://doi.org/10.5186/aasfm.2011.3628; https://repositorio.uc.cl/handle/11534/78663; WOS:000295069400005

الاتاحة: https://repositorio.uc.cl/handle/11534/78663
https://doi.org/10.5186/aasfm.2011.3628

المؤلفون: Chuaqui, Martin, Duren, Peter, Osgood, Brad, Stowe, Dennis

مصطلحات موضوعية: linear differential equations, zeros of solutions, oscillation, relative convexity, Sturm comparison theorem, Schwarzian derivative, univalence, CRITERIA

وصف الملف: 9 páginas; application/pdf

Relation: https://doi.org/10.1017/S0004972708001202; https://repositorio.uc.cl/handle/11534/76269; WOS:000265053300016

الاتاحة: https://repositorio.uc.cl/handle/11534/76269
https://doi.org/10.1017/S0004972708001202

المؤلفون: Tabareau, Nicolas, Tanter, Éric, Sozeau, Matthieu

المساهمون: Gallinette : vers une nouvelle génération d'assistant à la preuve (LS2N - équipe GALLINETTE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT), Département Automatique, Productique et Informatique (IMT Atlantique - DAPI), IMT Atlantique (IMT Atlantique), Universidad de Chile = University of Chile Santiago (UCHILE), European Project: 637339,H2020 ERC,ERC-2014-STG,CoqHoTT(2015)

المصدر: ISSN: 0004-5411.

مصطلحات موضوعية: Type theory, Type structures, Program reasoning Type Equivalence, Univalence, Parametricity, Proof Assistants, Coq, [MATH.MATH-CT]Mathematics [math]/Category Theory [math.CT]

Relation: info:eu-repo/grantAgreement//637339/EU/Coq for Homotopy Type Theory/CoqHoTT; hal-03120580; https://inria.hal.science/hal-03120580; https://inria.hal.science/hal-03120580/document; https://inria.hal.science/hal-03120580/file/main_jacm.pdf

الاتاحة: https://inria.hal.science/hal-03120580
https://inria.hal.science/hal-03120580/document
https://inria.hal.science/hal-03120580/file/main_jacm.pdf
https://doi.org/10.1145/3429979

المؤلفون: DONG, XIN-HAN, LAU, KA-SING, WU, HAI-HUA

المصدر: Transactions of the American Mathematical Society, 2017 Jul 01. 369(7), 4817-4842.

URL الوصول: https://www.jstor.org/stable/90006131

المؤلفون: Gowda, M. Seetharama, Sznajder, Roman

المصدر: Mathematics of Operations Research, 1999 Feb 01. 24(1), 255-261.

URL الوصول: https://www.jstor.org/stable/3690540

المؤلفون: Coquand, Thierry, Huber, Simon, Sattler, Christian

المساهمون: Thierry Coquand and Simon Huber and Christian Sattler

مصطلحات موضوعية: cubical type theory, univalence, canonicity, sconing, Artin glueing

وصف الملف: application/pdf

Relation: Is Part Of LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019); https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.11

الاتاحة: https://doi.org/10.4230/LIPIcs.FSCD.2019.11
https://nbn-resolving.org/urn:nbn:de:0030-drops-105188
https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.11

المؤلفون: Uemura, Taichi

المساهمون: Taichi Uemura

مصطلحات موضوعية: Cubical type theory, Realizability, Impredicative universe, Univalence, Propositional resizing

وصف الملف: application/pdf

Relation: Is Part Of LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018); https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.7

الاتاحة: https://doi.org/10.4230/LIPIcs.TYPES.2018.7
https://nbn-resolving.org/urn:nbn:de:0030-drops-114118
https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.7