Kraus, Nicolai; Nordvall Forsberg, Fredrik; Xu, Chuangjie Type-theoretic approaches to ordinals. (English) Zbl 07679991 Theor. Comput. Sci. 957, Article ID 113843, 34 p. (2023). MSC: 68Qxx PDF BibTeX XML Cite \textit{N. Kraus} et al., Theor. Comput. Sci. 957, Article ID 113843, 34 p. (2023; Zbl 07679991) Full Text: DOI arXiv OpenURL
Veltri, Niccolò; Vezzosi, Andrea Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda. (English) Zbl 07649243 J. Log. Algebr. Methods Program. 131, Article ID 100846, 23 p. (2023). MSC: 68-XX PDF BibTeX XML Cite \textit{N. Veltri} and \textit{A. Vezzosi}, J. Log. Algebr. Methods Program. 131, Article ID 100846, 23 p. (2023; Zbl 07649243) Full Text: DOI OpenURL
Stenzel, Raffael Univalence and completeness of Segal objects. (English) Zbl 1502.18048 J. Pure Appl. Algebra 227, No. 4, Article ID 107254, 47 p. (2023). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N45 18N50 18N60 18C50 55U35 PDF BibTeX XML Cite \textit{R. Stenzel}, J. Pure Appl. Algebra 227, No. 4, Article ID 107254, 47 p. (2023; Zbl 1502.18048) Full Text: DOI arXiv OpenURL
Kraus, Nicolai; von Raumer, Jakob A rewriting coherence theorem with applications in homotopy type theory. (English) Zbl 07657637 Math. Struct. Comput. Sci. 32, No. 7, 982-1014 (2022). MSC: 03B38 55U35 68Q42 PDF BibTeX XML Cite \textit{N. Kraus} and \textit{J. von Raumer}, Math. Struct. Comput. Sci. 32, No. 7, 982--1014 (2022; Zbl 07657637) Full Text: DOI arXiv OpenURL
Cottrell, Thomas; Fujii, Soichiro Hom weak \(\omega\)-categories of a weak \(\omega\)-category. (English) Zbl 07634873 Math. Struct. Comput. Sci. 32, No. 4, 420-441 (2022). MSC: 18-XX PDF BibTeX XML Cite \textit{T. Cottrell} and \textit{S. Fujii}, Math. Struct. Comput. Sci. 32, No. 4, 420--441 (2022; Zbl 07634873) Full Text: DOI arXiv OpenURL
Schroeder-Heister, Peter Axiomatic thinking, identity of proofs and the quest for an intensional proof-theoretic semantics. (English) Zbl 07633000 Ferreira, Fernando (ed.) et al., Axiomatic thinking I. Cham: Springer. 145-163 (2022). MSC: 03-03 03A05 00A30 01A80 01A60 PDF BibTeX XML Cite \textit{P. Schroeder-Heister}, in: Axiomatic thinking I. Cham: Springer. 145--163 (2022; Zbl 07633000) Full Text: DOI OpenURL
Popescu, Andrei Rensets and renaming-based recursion for syntax with bindings. (English) Zbl 07628212 Blanchette, Jasmin (ed.) et al., Automated reasoning. 11th international joint conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13385, 618-639 (2022). MSC: 68V15 PDF BibTeX XML Cite \textit{A. Popescu}, Lect. Notes Comput. Sci. 13385, 618--639 (2022; Zbl 07628212) Full Text: DOI arXiv OpenURL
Shulman, Michael Affine logic for constructive mathematics. (English) Zbl 07606771 Bull. Symb. Log. 28, No. 3, 327-386 (2022). MSC: 03F52 03F65 PDF BibTeX XML Cite \textit{M. Shulman}, Bull. Symb. Log. 28, No. 3, 327--386 (2022; Zbl 07606771) Full Text: DOI arXiv OpenURL
Crosilla, Laura Predicativity and constructive mathematics. (English) Zbl 07598443 Oliveri, Gianluigi (ed.) et al., Objects, structures, and logics. FilMat studies in the philosophy of mathematics. Cham: Springer. Boston Stud. Philos. Hist. Sci. 339, 287-309 (2022). MSC: 03-XX 00A30 PDF BibTeX XML Cite \textit{L. Crosilla}, Boston Stud. Philos. Hist. Sci. 339, 287--309 (2022; Zbl 07598443) Full Text: DOI OpenURL
Marquis, Jean-Pierre The structuralist mathematical style: Bourbaki as a case study. (English) Zbl 07598440 Oliveri, Gianluigi (ed.) et al., Objects, structures, and logics. FilMat studies in the philosophy of mathematics. Cham: Springer. Boston Stud. Philos. Hist. Sci. 339, 199-231 (2022). MSC: 03-XX 00A30 PDF BibTeX XML Cite \textit{J.-P. Marquis}, Boston Stud. Philos. Hist. Sci. 339, 199--231 (2022; Zbl 07598440) Full Text: DOI OpenURL
Tohmé, Fernando; Caterina, Gianluca; Gangle, Rocco Observability in the univalent universe. (English) Zbl 07592507 Mediterr. J. Math. 19, No. 5, Paper No. 216, 19 p. (2022). MSC: 03-XX 68-XX PDF BibTeX XML Cite \textit{F. Tohmé} et al., Mediterr. J. Math. 19, No. 5, Paper No. 216, 19 p. (2022; Zbl 07592507) Full Text: DOI OpenURL
Myers, David Jaz Good fibrations through the modal prism. (English) Zbl 1502.18047 High. Struct. 6, No. 1, 212-255 (2022). Reviewer: Daniel Graves (Leeds) MSC: 18N45 03B38 55U35 PDF BibTeX XML Cite \textit{D. J. Myers}, High. Struct. 6, No. 1, 212--255 (2022; Zbl 1502.18047) Full Text: arXiv Link OpenURL
Sterling, Jonathan; Angiuli, Carlo; Gratzer, Daniel A cubical language for Bishop sets. (English) Zbl 07566056 Log. Methods Comput. Sci. 18, No. 1, Paper No. 43, 80 p. (2022). MSC: 03B70 68-XX PDF BibTeX XML Cite \textit{J. Sterling} et al., Log. Methods Comput. Sci. 18, No. 1, Paper No. 43, 80 p. (2022; Zbl 07566056) Full Text: arXiv Link OpenURL
Emmenegger, Jacopo; Pasquali, Fabio; Rosolini, Giuseppe A characterisation of elementary fibrations. (English) Zbl 1492.18008 Ann. Pure Appl. Logic 173, No. 6, Article ID 103103, 29 p. (2022). Reviewer: Robert Rosebrugh (Sackville) MSC: 18C40 18C50 03G30 18D30 18D40 18N45 PDF BibTeX XML Cite \textit{J. Emmenegger} et al., Ann. Pure Appl. Logic 173, No. 6, Article ID 103103, 29 p. (2022; Zbl 1492.18008) Full Text: DOI arXiv OpenURL
Anel, Mathieu; Biedermann, Georg; Finster, Eric; Joyal, André Left-exact localizations of \(\infty\)-topoi. I: Higher sheaves. (English) Zbl 1498.18009 Adv. Math. 400, Article ID 108268, 64 p. (2022). Reviewer: Markus Szymik (Sheffield) MSC: 18F20 18N60 18N55 PDF BibTeX XML Cite \textit{M. Anel} et al., Adv. Math. 400, Article ID 108268, 64 p. (2022; Zbl 1498.18009) Full Text: DOI arXiv OpenURL
Barton, Neil; Müller, Moritz; Prunescu, Mihai On representations of intended structures in foundational theories. (English) Zbl 07502595 J. Philos. Log. 51, No. 2, 283-296 (2022). MSC: 03-XX PDF BibTeX XML Cite \textit{N. Barton} et al., J. Philos. Log. 51, No. 2, 283--296 (2022; Zbl 07502595) Full Text: DOI OpenURL
Coquand, Thierry; Huber, Simon; Sattler, Christian Canonicity and homotopy canonicity for cubical type theory. (English) Zbl 1486.03027 Log. Methods Comput. Sci. 18, No. 1, Paper No. 28, 35 p. (2022). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 03B38 03G30 55U35 PDF BibTeX XML Cite \textit{T. Coquand} et al., Log. Methods Comput. Sci. 18, No. 1, Paper No. 28, 35 p. (2022; Zbl 1486.03027) Full Text: arXiv Link OpenURL
Swan, Andrew W. On the Nielsen-Schreier theorem in homotopy type theory. (English) Zbl 07471707 Log. Methods Comput. Sci. 18, No. 1, Paper No. 18, 15 p. (2022). MSC: 03B70 68-XX PDF BibTeX XML Cite \textit{A. W. Swan}, Log. Methods Comput. Sci. 18, No. 1, Paper No. 18, 15 p. (2022; Zbl 07471707) Full Text: arXiv Link OpenURL
Christensen, J. Daniel; Rijke, Egbert Characterizations of modalities and lex modalities. (English) Zbl 1482.18015 J. Pure Appl. Algebra 226, No. 3, Article ID 106848, 21 p. (2022). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N55 03B38 03B45 03G30 18N60 55P60 PDF BibTeX XML Cite \textit{J. D. Christensen} and \textit{E. Rijke}, J. Pure Appl. Algebra 226, No. 3, Article ID 106848, 21 p. (2022; Zbl 1482.18015) Full Text: DOI arXiv OpenURL
Angere, Staffan Identity and intensionality in univalent foundations and philosophy. (English) Zbl 1507.03008 Synthese 198, Suppl. 5, S1177-S1217 (2021). MSC: 03A05 03B38 55U35 00A30 PDF BibTeX XML Cite \textit{S. Angere}, Synthese 198, S1177--S1217 (2021; Zbl 1507.03008) Full Text: DOI OpenURL
Bidlingmaier, Martin E.; Faissole, Florian; Spitters, Bas Synthetic topology in homotopy type theory for probabilistic programming. (English) Zbl 07630477 Math. Struct. Comput. Sci. 31, No. 10, 1301-1329 (2021). MSC: 68-XX PDF BibTeX XML Cite \textit{M. E. Bidlingmaier} et al., Math. Struct. Comput. Sci. 31, No. 10, 1301--1329 (2021; Zbl 07630477) Full Text: DOI arXiv OpenURL
de Jong, Tom The Scott model of PCF in univalent type theory. (English) Zbl 07630476 Math. Struct. Comput. Sci. 31, No. 10, 1270-1300 (2021). MSC: 68-XX PDF BibTeX XML Cite \textit{T. de Jong}, Math. Struct. Comput. Sci. 31, No. 10, 1270--1300 (2021; Zbl 07630476) Full Text: DOI arXiv OpenURL
Ahrens, Benedikt; Frumin, Dan; Maggesi, Marco; Veltri, Niccolò; van der Weide, Niels Bicategories in univalent foundations. (English) Zbl 07630475 Math. Struct. Comput. Sci. 31, No. 10, 1232-1269 (2021). MSC: 68-XX PDF BibTeX XML Cite \textit{B. Ahrens} et al., Math. Struct. Comput. Sci. 31, No. 10, 1232--1269 (2021; Zbl 07630475) Full Text: DOI OpenURL
Bentzen, Bruno Naive cubical type theory. (English) Zbl 07630474 Math. Struct. Comput. Sci. 31, No. 10, 1205-1231 (2021). MSC: 68-XX PDF BibTeX XML Cite \textit{B. Bentzen}, Math. Struct. Comput. Sci. 31, No. 10, 1205--1231 (2021; Zbl 07630474) Full Text: DOI arXiv OpenURL
Swan, Andrew W.; Uemura, Taichi On Church’s thesis in cubical assemblies. (English) Zbl 07630473 Math. Struct. Comput. Sci. 31, No. 10, 1185-1204 (2021). MSC: 68-XX PDF BibTeX XML Cite \textit{A. W. Swan} and \textit{T. Uemura}, Math. Struct. Comput. Sci. 31, No. 10, 1185--1204 (2021; Zbl 07630473) Full Text: DOI arXiv OpenURL
Mörtberg, Anders Cubical methods in homotopy type theory and univalent foundations. (English) Zbl 07630472 Math. Struct. Comput. Sci. 31, No. 10, 1147-1184 (2021). MSC: 68-XX PDF BibTeX XML Cite \textit{A. Mörtberg}, Math. Struct. Comput. Sci. 31, No. 10, 1147--1184 (2021; Zbl 07630472) Full Text: DOI OpenURL
Altenkirch, Thorsten Martin Hofmann’s contributions to type theory: groupoids and univalence. (English) Zbl 1496.03003 Math. Struct. Comput. Sci. 31, No. 9, 953-957 (2021). MSC: 03-03 01A70 03B38 PDF BibTeX XML Cite \textit{T. Altenkirch}, Math. Struct. Comput. Sci. 31, No. 9, 953--957 (2021; Zbl 1496.03003) Full Text: DOI OpenURL
Turner, D. A. Constructive mathematics, Church’s thesis, and free choice sequences. (English) Zbl 07495191 De Mol, Liesbeth (ed.) et al., Connecting with computability. 17th conference on computability in Europe, CiE 2021, virtual event, Ghent, Belgium, July 5–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12813, 446-456 (2021). MSC: 68Qxx PDF BibTeX XML Cite \textit{D. A. Turner}, Lect. Notes Comput. Sci. 12813, 446--456 (2021; Zbl 07495191) Full Text: DOI Link OpenURL
Cavallo, Evan; Harper, Robert Internal parametricity for cubical type theory. (English) Zbl 07471665 Log. Methods Comput. Sci. 17, No. 4, Paper No. 5, 60 p. (2021). Reviewer: Jonathan Weinberger (Baltimore) MSC: 03B38 PDF BibTeX XML Cite \textit{E. Cavallo} and \textit{R. Harper}, Log. Methods Comput. Sci. 17, No. 4, Paper No. 5, 60 p. (2021; Zbl 07471665) Full Text: arXiv Link OpenURL
Cherubini, Felix; Rijke, Egbert Modal descent. (English) Zbl 1481.18029 Math. Struct. Comput. Sci. 31, No. 4, 363-391 (2021). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N45 03B38 03B10 PDF BibTeX XML Cite \textit{F. Cherubini} and \textit{E. Rijke}, Math. Struct. Comput. Sci. 31, No. 4, 363--391 (2021; Zbl 1481.18029) Full Text: DOI arXiv OpenURL
Vezzosi, Andrea; Mörtberg, Anders; Abel, Andreas Cubical agda: a dependently typed programming language with univalence and higher inductive types. (English) Zbl 07443766 J. Funct. Program. 31, Paper No. e8, 47 p. (2021). MSC: 68N18 PDF BibTeX XML Cite \textit{A. Vezzosi} et al., J. Funct. Program. 31, Paper No. e8, 47 p. (2021; Zbl 07443766) Full Text: DOI OpenURL
Ellerman, David On abstraction in mathematics and indefiniteness in quantum mechanics. (English) Zbl 07413738 J. Philos. Log. 50, No. 4, 813-835 (2021). MSC: 03-XX PDF BibTeX XML Cite \textit{D. Ellerman}, J. Philos. Log. 50, No. 4, 813--835 (2021; Zbl 07413738) Full Text: DOI Link OpenURL
Altenkirch, Thorsten; Boulier, Simon; Kaposi, Ambrus; Sattler, Christian; Sestini, Filippo Constructing a universe for the setoid model. (English) Zbl 07410416 Kiefer, Stefan (ed.) et al., Foundations of software science and computation structures. 24th international conference, FOSSACS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12650, 1-21 (2021). MSC: 68Nxx 68Qxx PDF BibTeX XML Cite \textit{T. Altenkirch} et al., Lect. Notes Comput. Sci. 12650, 1--21 (2021; Zbl 07410416) Full Text: DOI OpenURL
Gallozzi, Cesare Homotopy type-theoretic interpretations of constructive set theories. (English) Zbl 07408498 Math. Struct. Comput. Sci. 31, No. 1, 112-143 (2021). MSC: 03B38 03E70 18N45 PDF BibTeX XML Cite \textit{C. Gallozzi}, Math. Struct. Comput. Sci. 31, No. 1, 112--143 (2021; Zbl 07408498) Full Text: DOI OpenURL
Hötzel Escardó, Martín Injective types in univalent mathematics. (English) Zbl 1478.18025 Math. Struct. Comput. Sci. 31, No. 1, 89-111 (2021). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N45 03B38 PDF BibTeX XML Cite \textit{M. Hötzel Escardó}, Math. Struct. Comput. Sci. 31, No. 1, 89--111 (2021; Zbl 1478.18025) Full Text: DOI arXiv OpenURL
Isaev, Valery Indexed type theories. (English) Zbl 1494.18018 Math. Struct. Comput. Sci. 31, No. 1, 3-63 (2021). Reviewer: Marco Benini (Como) MSC: 18N45 03B38 55U35 PDF BibTeX XML Cite \textit{V. Isaev}, Math. Struct. Comput. Sci. 31, No. 1, 3--63 (2021; Zbl 1494.18018) Full Text: DOI arXiv OpenURL
Emmenegger, Jacopo W-types in setoids. (English) Zbl 1505.03029 Log. Methods Comput. Sci. 17, No. 3, Paper No. 28, 33 p. (2021). Reviewer: Jonathan Sterling (Aarhus) MSC: 03B38 03B35 PDF BibTeX XML Cite \textit{J. Emmenegger}, Log. Methods Comput. Sci. 17, No. 3, Paper No. 28, 33 p. (2021; Zbl 1505.03029) Full Text: arXiv Link OpenURL
Gratzer, Daniel; Kavvos, G. A.; Nuyts, Andreas; Birkedal, Lars Multimodal dependent type theory. (English) Zbl 1498.03030 Log. Methods Comput. Sci. 17, No. 3, Paper No. 11, 67 p. (2021). MSC: 03B38 03B45 PDF BibTeX XML Cite \textit{D. Gratzer} et al., Log. Methods Comput. Sci. 17, No. 3, Paper No. 11, 67 p. (2021; Zbl 1498.03030) Full Text: arXiv Link OpenURL
Hötzel Escardó, Martín The Cantor-Schröder-Bernstein theorem for \(\infty\)-groupoids. (English) Zbl 07402358 J. Homotopy Relat. Struct. 16, No. 3, 363-366 (2021). MSC: 03-XX 55U40 03B15 03F55 03B38 PDF BibTeX XML Cite \textit{M. Hötzel Escardó}, J. Homotopy Relat. Struct. 16, No. 3, 363--366 (2021; Zbl 07402358) Full Text: DOI arXiv OpenURL
Rasekh, Nima Filter quotients and non-presentable \((\infty,1)\)-toposes. (English) Zbl 1467.18045 J. Pure Appl. Algebra 225, No. 12, Article ID 106770, 36 p. (2021). Reviewer: Philippe Gaucher (Paris) MSC: 18N60 18B25 18N45 55U35 PDF BibTeX XML Cite \textit{N. Rasekh}, J. Pure Appl. Algebra 225, No. 12, Article ID 106770, 36 p. (2021; Zbl 1467.18045) Full Text: DOI arXiv OpenURL
Kapulkin, Krzysztof; Lumsdaine, Peter Lefanu The simplicial model of univalent foundations (after Voevodsky). (English) Zbl 1471.18025 J. Eur. Math. Soc. (JEMS) 23, No. 6, 2071-2126 (2021). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N45 18C50 55U10 55U35 PDF BibTeX XML Cite \textit{K. Kapulkin} and \textit{P. L. Lumsdaine}, J. Eur. Math. Soc. (JEMS) 23, No. 6, 2071--2126 (2021; Zbl 1471.18025) Full Text: DOI arXiv OpenURL
Bezem, Marc; Buchholtz, Ulrik; Grayson, Daniel R.; Shulman, Michael Construction of the circle in UniMath. (English) Zbl 07357172 J. Pure Appl. Algebra 225, No. 10, Article ID 106687, 21 p. (2021). MSC: 03B38 03B70 55U35 03G30 PDF BibTeX XML Cite \textit{M. Bezem} et al., J. Pure Appl. Algebra 225, No. 10, Article ID 106687, 21 p. (2021; Zbl 07357172) Full Text: DOI arXiv OpenURL
Kapulkin, Krzysztof; Lumsdaine, Peter LeFanu Homotopical inverse diagrams in categories with attributes. (English) Zbl 1453.18007 J. Pure Appl. Algebra 225, No. 4, Article ID 106563, 44 p. (2021). Reviewer: Panagis Karazeris (Patras) MSC: 18C50 03B38 03G30 PDF BibTeX XML Cite \textit{K. Kapulkin} and \textit{P. L. Lumsdaine}, J. Pure Appl. Algebra 225, No. 4, Article ID 106563, 44 p. (2021; Zbl 1453.18007) Full Text: DOI arXiv OpenURL
Tsementzis, Dimitris A meaning explanation for HoTT. (English) Zbl 1475.03055 Synthese 197, No. 2, 651-680 (2020). MSC: 03A05 03B38 55U35 PDF BibTeX XML Cite \textit{D. Tsementzis}, Synthese 197, No. 2, 651--680 (2020; Zbl 1475.03055) Full Text: DOI Link OpenURL
Lumsdaine, Peter Lefanu; Shulman, Michael Semantics of higher inductive types. (English) Zbl 1470.18007 Math. Proc. Camb. Philos. Soc. 169, No. 1, 159-208 (2020). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18C50 03B38 18N40 18N45 18N60 PDF BibTeX XML Cite \textit{P. L. Lumsdaine} and \textit{M. Shulman}, Math. Proc. Camb. Philos. Soc. 169, No. 1, 159--208 (2020; Zbl 1470.18007) Full Text: DOI arXiv Backlinks: MO OpenURL
Huguenin-Dumittan, Loïs; Vaudenay, Serge Classical misuse attacks on NIST round 2 PQC. The power of rank-based schemes. (English) Zbl 07314284 Conti, Mauro (ed.) et al., Applied cryptography and network security. 18th international conference, ACNS 2020, Rome, Italy, October 19–22, 2020. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12146, 208-227 (2020). MSC: 68M25 94A60 PDF BibTeX XML Cite \textit{L. Huguenin-Dumittan} and \textit{S. Vaudenay}, Lect. Notes Comput. Sci. 12146, 208--227 (2020; Zbl 07314284) Full Text: DOI OpenURL
Scoccola, Luis Nilpotent types and fracture squares in homotopy type theory. (English) Zbl 1498.18038 Math. Struct. Comput. Sci. 30, No. 5, 511-544 (2020). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N45 03B70 55P60 18E35 PDF BibTeX XML Cite \textit{L. Scoccola}, Math. Struct. Comput. Sci. 30, No. 5, 511--544 (2020; Zbl 1498.18038) Full Text: DOI arXiv OpenURL
Doczkal, Christian; Pous, Damien Graph theory in Coq: minors, treewidth, and isomorphisms. (English) Zbl 1468.68320 J. Autom. Reasoning 64, No. 5, 795-825 (2020). MSC: 68V20 03B35 05C05 05C40 05C60 05C83 PDF BibTeX XML Cite \textit{C. Doczkal} and \textit{D. Pous}, J. Autom. Reasoning 64, No. 5, 795--825 (2020; Zbl 1468.68320) Full Text: DOI HAL OpenURL
van den Berg, Benno Univalent polymorphism. (English) Zbl 1440.18048 Ann. Pure Appl. Logic 171, No. 6, Article ID 102793, 29 p. (2020). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N45 03B38 03F50 03G30 18C50 55U35 68Q55 PDF BibTeX XML Cite \textit{B. van den Berg}, Ann. Pure Appl. Logic 171, No. 6, Article ID 102793, 29 p. (2020; Zbl 1440.18048) Full Text: DOI arXiv OpenURL
Roberts, Bryan W.; Weatherall, James Owen New perspectives on the hole argument. (English) Zbl 1436.83013 Found. Phys. 50, No. 4, 217-227 (2020). MSC: 83C05 83E05 00A30 83-03 01A60 PDF BibTeX XML Cite \textit{B. W. Roberts} and \textit{J. O. Weatherall}, Found. Phys. 50, No. 4, 217--227 (2020; Zbl 1436.83013) Full Text: DOI OpenURL
Christensen, J. Daniel; Peck Opie, Morgan; Rijke, Egbert; Scoccola, Luis Nerio Localization in homotopy type theory. (English) Zbl 1439.18023 High. Struct. 4, No. 1, 1-32 (2020). MSC: 18N45 18E35 03B38 55P60 PDF BibTeX XML Cite \textit{J. D. Christensen} et al., High. Struct. 4, No. 1, 1--32 (2020; Zbl 1439.18023) Full Text: arXiv OpenURL
Kaposi, Ambrus; Kovács, András Signatures and induction principles for higher inductive-inductive types. (English) Zbl 07168146 Log. Methods Comput. Sci. 16, No. 1, Paper No. 10, 30 p. (2020). MSC: 03B70 68-XX PDF BibTeX XML Cite \textit{A. Kaposi} and \textit{A. Kovács}, Log. Methods Comput. Sci. 16, No. 1, Paper No. 10, 30 p. (2020; Zbl 07168146) Full Text: arXiv OpenURL
Ringer, Talia; Yazdani, Nathaniel; Leo, John; Grossman, Dan Ornaments for proof reuse in Coq. (English) Zbl 07649975 Harrison, John (ed.) et al., 10th international conference on interactive theorem proving, ITP 2019, September 9–12, 2019, Portland, OR, USA. Proceedings. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 141, Article 26, 19 p. (2019). MSC: 68T15 PDF BibTeX XML Cite \textit{T. Ringer} et al., LIPIcs -- Leibniz Int. Proc. Inform. 141, Article 26, 19 p. (2019; Zbl 07649975) Full Text: DOI OpenURL
Uemura, Taichi Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing. (English) Zbl 07561492 Dybjer, Peter (ed.) et al., 24th international conference on types for proofs and programs, TYPES 2018, Braga, Portugal, June 18–21, 2018. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 130, Article 7, 20 p. (2019). MSC: 03B70 68N30 PDF BibTeX XML Cite \textit{T. Uemura}, LIPIcs -- Leibniz Int. Proc. Inform. 130, Article 7, 20 p. (2019; Zbl 07561492) Full Text: DOI arXiv OpenURL
Petrakis, Iosif Dependent sums and dependent products in Bishop’s set theory. (English) Zbl 07561488 Dybjer, Peter (ed.) et al., 24th international conference on types for proofs and programs, TYPES 2018, Braga, Portugal, June 18–21, 2018. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 130, Article 3, 21 p. (2019). MSC: 03B70 68N30 PDF BibTeX XML Cite \textit{I. Petrakis}, LIPIcs -- Leibniz Int. Proc. Inform. 130, Article 3, 21 p. (2019; Zbl 07561488) Full Text: DOI OpenURL
Sterling, Jonathan; Angiuli, Carlo; Gratzer, Daniel Cubical syntax for reflection-free extensional equality. (English) Zbl 07559297 Geuvers, Herman (ed.), 4th international conference on formal structures for computation and deduction, FSCD 2019, Dortmund, Germany, June 24–30, 2019. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 131, Article 31, 25 p. (2019). MSC: 03B70 68Qxx PDF BibTeX XML Cite \textit{J. Sterling} et al., LIPIcs -- Leibniz Int. Proc. Inform. 131, Article 31, 25 p. (2019; Zbl 07559297) Full Text: DOI arXiv OpenURL
Díaz-Caro, Alejandro; Dowek, Gilles Proof normalisation in a logic identifying isomorphic propositions. (English) Zbl 07559280 Geuvers, Herman (ed.), 4th international conference on formal structures for computation and deduction, FSCD 2019, Dortmund, Germany, June 24–30, 2019. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 131, Article 14, 23 p. (2019). MSC: 03B70 68Qxx PDF BibTeX XML Cite \textit{A. Díaz-Caro} and \textit{G. Dowek}, LIPIcs -- Leibniz Int. Proc. Inform. 131, Article 14, 23 p. (2019; Zbl 07559280) Full Text: DOI arXiv OpenURL
Coquand, Thierry; Huber, Simon; Sattler, Christian Homotopy canonicity for cubical type theory. (English) Zbl 07559277 Geuvers, Herman (ed.), 4th international conference on formal structures for computation and deduction, FSCD 2019, Dortmund, Germany, June 24–30, 2019. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 131, Article 11, 23 p. (2019). MSC: 03B70 68Qxx PDF BibTeX XML Cite \textit{T. Coquand} et al., LIPIcs -- Leibniz Int. Proc. Inform. 131, Article 11, 23 p. (2019; Zbl 07559277) Full Text: DOI OpenURL
Ahrens, Benedikt; Frumin, Dan; Maggesi, Marco; van der Weide, Niels Bicategories in univalent foundations. (English) Zbl 07559271 Geuvers, Herman (ed.), 4th international conference on formal structures for computation and deduction, FSCD 2019, Dortmund, Germany, June 24–30, 2019. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 131, Article 5, 17 p. (2019). MSC: 03B70 68Qxx PDF BibTeX XML Cite \textit{B. Ahrens} et al., LIPIcs -- Leibniz Int. Proc. Inform. 131, Article 5, 17 p. (2019; Zbl 07559271) Full Text: DOI arXiv OpenURL
van der Weide, Niels; Geuvers, Herman The construction of set-truncated higher inductive types. (English) Zbl 07515964 König, Barbara (ed.), Proceedings of the 35th conference on the mathematical foundations of programming semantics, MFPS XXXV, London, UK, June 4–7, 2019. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 347, 261-280 (2019). MSC: 68N30 68Q55 PDF BibTeX XML Cite \textit{N. van der Weide} and \textit{H. Geuvers}, Electron. Notes Theor. Comput. Sci. 347, 261--280 (2019; Zbl 07515964) Full Text: DOI OpenURL
Alessi, Fabio; Ciaffaglione, Alberto; Di Gianantonio, Pietro; Honsell, Furio; Lenisa, Marina; Scagnetto, Ivan \(\mathrm{LF}^+\) in Coq for fast-and-loose reasoning. (English) Zbl 1427.68344 J. Formaliz. Reason. 12, 11-51 (2019). MSC: 68V15 03B38 03B70 68V20 PDF BibTeX XML Cite \textit{F. Alessi} et al., J. Formaliz. Reason. 12, 11--51 (2019; Zbl 1427.68344) Full Text: DOI OpenURL
Gunther, Emmanuel; Pagano, Miguel; Sánchez Terraf, Pedro First steps towards a formalization of forcing. (English) Zbl 1434.03029 Accattoli, Beniamino (ed.) et al., Proceedings of the 13th workshop on logical and semantic frameworks with applications, LSFA 18, Fortaleza, Brazil, September 26–28, 2018. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 344, 119-136 (2019). MSC: 03B35 03E35 68V20 PDF BibTeX XML Cite \textit{E. Gunther} et al., Electron. Notes Theor. Comput. Sci. 344, 119--136 (2019; Zbl 1434.03029) Full Text: DOI arXiv OpenURL
Ahrens, Benedikt; Matthes, Ralph; Mörtberg, Anders From signatures to monads in UniMath. (English) Zbl 1468.03007 J. Autom. Reasoning 63, No. 2, 285-318 (2019). MSC: 03B35 03B38 18C10 18C15 55U35 68V20 PDF BibTeX XML Cite \textit{B. Ahrens} et al., J. Autom. Reasoning 63, No. 2, 285--318 (2019; Zbl 1468.03007) Full Text: DOI arXiv OpenURL
Romero, Ana; Rubio, Julio; Sergeraert, Francis An implementation of effective homotopy of fibrations. (English) Zbl 1436.55022 J. Symb. Comput. 94, 149-172 (2019). MSC: 55R05 68W30 PDF BibTeX XML Cite \textit{A. Romero} et al., J. Symb. Comput. 94, 149--172 (2019; Zbl 1436.55022) Full Text: DOI OpenURL
Kapulkin, Krzysztof; Szumiło, Karol Internal languages of finitely complete \((\infty , 1)\)-categories. (English) Zbl 1462.18007 Sel. Math., New Ser. 25, No. 2, Paper No. 33, 46 p. (2019). Reviewer: Julie Bergner (Riverside) MSC: 18N60 55U35 03B38 PDF BibTeX XML Cite \textit{K. Kapulkin} and \textit{K. Szumiło}, Sel. Math., New Ser. 25, No. 2, Paper No. 33, 46 p. (2019; Zbl 1462.18007) Full Text: DOI arXiv OpenURL
Gauthier, Thibault; Kaliszyk, Cezary Aligning concepts across proof assistant libraries. (English) Zbl 1395.68247 J. Symb. Comput. 90, 89-123 (2019). MSC: 68T15 PDF BibTeX XML Cite \textit{T. Gauthier} and \textit{C. Kaliszyk}, J. Symb. Comput. 90, 89--123 (2019; Zbl 1395.68247) Full Text: DOI OpenURL
Angiuli, Carlo; Hou, (Favonia) Kuen-Bang; Harper, Robert Cartesian cubical computational type theory: constructive reasoning with paths and equalities. (English) Zbl 07533331 Ghica, Dan R. (ed.) et al., 27th EACSL annual conference on computer science logic, CSL 2018, Birmingham, United Kingdom, September 4–8, 2018. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 119, Article 6, 17 p. (2018). MSC: 03B70 PDF BibTeX XML Cite \textit{C. Angiuli} et al., LIPIcs -- Leibniz Int. Proc. Inform. 119, Article 6, 17 p. (2018; Zbl 07533331) Full Text: DOI OpenURL
Carette, Jacques; Chen, Chao-Hong; Choudhury, Vikraman; Sabry, Amr From reversible programs to univalent universes and back. (English) Zbl 07513452 Silva, Alexandra (ed.), Proceedings of the 33rd conference on the mathematical foundations of programming semantics (MFPS XXXIII), Ljubljana, Slovenia, June 12–15, 2017. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 336, 5-25 (2018). MSC: 68N30 68Q55 PDF BibTeX XML Cite \textit{J. Carette} et al., Electron. Notes Theor. Comput. Sci. 336, 5--25 (2018; Zbl 07513452) Full Text: DOI arXiv OpenURL
Dougherty, John What inductive explanations could not be. (English) Zbl 1452.00012 Synthese 195, No. 12, 5473-5483 (2018). MSC: 00A30 03A05 PDF BibTeX XML Cite \textit{J. Dougherty}, Synthese 195, No. 12, 5473--5483 (2018; Zbl 1452.00012) Full Text: DOI Link OpenURL
Affeldt, Reynald; Cohen, Cyril; Rouhling, Damien Formalization techniques for asymptotic reasoning in classical analysis. (English) Zbl 1451.68329 J. Formaliz. Reason. 11, 43-76 (2018). MSC: 68V20 26A03 PDF BibTeX XML Cite \textit{R. Affeldt} et al., J. Formaliz. Reason. 11, 43--76 (2018; Zbl 1451.68329) Full Text: DOI OpenURL
Coquand, Thierry Combinatorial topology and constructive mathematics. (English) Zbl 06948560 Indag. Math., New Ser. 29, No. 6, 1637-1648 (2018). MSC: 03-XX 68-XX 54-XX PDF BibTeX XML Cite \textit{T. Coquand}, Indag. Math., New Ser. 29, No. 6, 1637--1648 (2018; Zbl 06948560) Full Text: DOI OpenURL
Kapulkin, Krzysztof; Lumsdaine, Peter LeFanu The homotopy theory of type theories. (English) Zbl 1397.18015 Adv. Math. 337, 1-38 (2018). Reviewer: Philippe Gaucher (Paris) MSC: 18C50 18G55 55U35 03B15 PDF BibTeX XML Cite \textit{K. Kapulkin} and \textit{P. L. Lumsdaine}, Adv. Math. 337, 1--38 (2018; Zbl 1397.18015) Full Text: DOI arXiv OpenURL
Grayson, Daniel R. An introduction to univalent foundations for mathematicians. (English) Zbl 1461.03012 Bull. Am. Math. Soc., New Ser. 55, No. 4, 427-450 (2018). MSC: 03B38 03B35 03G30 18A15 55U35 PDF BibTeX XML Cite \textit{D. R. Grayson}, Bull. Am. Math. Soc., New Ser. 55, No. 4, 427--450 (2018; Zbl 1461.03012) Full Text: DOI arXiv OpenURL
Ahrens, Benedikt; Lumsdaine, Peter Lefanu; Voevodsky, Vladimir Categorical structures for type theory in univalent foundations. (English) Zbl 1496.03053 Log. Methods Comput. Sci. 14, No. 3, Paper No. 18, 18 p. (2018). MSC: 03B38 03F50 18C50 03B70 55U40 68V15 PDF BibTeX XML Cite \textit{B. Ahrens} et al., Log. Methods Comput. Sci. 14, No. 3, Paper No. 18, 18 p. (2018; Zbl 1496.03053) Full Text: DOI arXiv OpenURL
van den Berg, Benno; Moerdijk, Ieke Univalent completion. (English) Zbl 1400.55007 Math. Ann. 371, No. 3-4, 1337-1350 (2018). Reviewer: Thomas Huettemann (Belfast) MSC: 55R15 55U10 18C50 PDF BibTeX XML Cite \textit{B. van den Berg} and \textit{I. Moerdijk}, Math. Ann. 371, No. 3--4, 1337--1350 (2018; Zbl 1400.55007) Full Text: DOI arXiv OpenURL
Gálvez-Carrillo, Imma; Kock, Joachim; Tonks, Andrew Decomposition spaces, incidence algebras and Möbius inversion. I: Basic theory. (English) Zbl 1403.00023 Adv. Math. 331, 952-1015 (2018). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 00B15 PDF BibTeX XML Cite \textit{I. Gálvez-Carrillo} et al., Adv. Math. 331, 952--1015 (2018; Zbl 1403.00023) Full Text: DOI arXiv Link OpenURL
Catren, Gabriel Klein-Weyl’s program and the ontology of gauge and quantum systems. (English) Zbl 1382.81009 Stud. Hist. Philos. Sci., Part B, Stud. Hist. Philos. Mod. Phys. 61, 25-40 (2018). MSC: 81P05 00A79 00A30 70S15 81T13 83A05 83C05 81R05 PDF BibTeX XML Cite \textit{G. Catren}, Stud. Hist. Philos. Sci., Part B, Stud. Hist. Philos. Mod. Phys. 61, 25--40 (2018; Zbl 1382.81009) Full Text: DOI OpenURL
Awodey, Steve Natural models of homotopy type theory. (English) Zbl 1456.03023 Math. Struct. Comput. Sci. 28, No. 2, 241-286 (2018). MSC: 03B38 55U35 18D15 18F20 PDF BibTeX XML Cite \textit{S. Awodey}, Math. Struct. Comput. Sci. 28, No. 2, 241--286 (2018; Zbl 1456.03023) Full Text: DOI arXiv OpenURL
Uustalu, Tarmo; Veltri, Niccolò Partiality and container monads. (English) Zbl 1503.03022 Chang, Bor-Yuh Evan (ed.), Programming languages and systems. 15th Asian symposium, APLAS 2017, Suzhou, China, November 27–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10695, 406-425 (2017). MSC: 03B38 03B70 18C15 PDF BibTeX XML Cite \textit{T. Uustalu} and \textit{N. Veltri}, Lect. Notes Comput. Sci. 10695, 406--425 (2017; Zbl 1503.03022) Full Text: DOI OpenURL
Bauer, Andrej Five stages of accepting constructive mathematics. (English) Zbl 1469.03171 Bull. Am. Math. Soc., New Ser. 54, No. 3, 481-498 (2017). MSC: 03F65 PDF BibTeX XML Cite \textit{A. Bauer}, Bull. Am. Math. Soc., New Ser. 54, No. 3, 481--498 (2017; Zbl 1469.03171) Full Text: DOI OpenURL
Ahrens, Benedikt; Lumsdaine, Peter LeFanu Displayed categories. (English) Zbl 1434.18002 Miller, Dale (ed.), 2nd international conference on formal structures for computation and deduction. FSCD 2017, Oxford, UK, September 3–9, 2017. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 84, Article 5, 16 p. (2017). MSC: 18A15 03B38 PDF BibTeX XML Cite \textit{B. Ahrens} and \textit{P. L. Lumsdaine}, LIPIcs -- Leibniz Int. Proc. Inform. 84, Article 5, 16 p. (2017; Zbl 1434.18002) Full Text: DOI OpenURL
Rathjen, Michael Proof theory of constructive systems: inductive types and univalence. (English) Zbl 1429.03213 Jäger, Gerhard (ed.) et al., Feferman on foundations. Logic, mathematics, philosophy. Cham: Springer. Outst. Contrib. Log. 13, 385-419 (2017). MSC: 03F50 03F30 03C62 03F35 03B38 PDF BibTeX XML Cite \textit{M. Rathjen}, Outst. Contrib. Log. 13, 385--419 (2017; Zbl 1429.03213) Full Text: DOI arXiv OpenURL
Crespo, Ricardo; Tohmé, Fernando The future of mathematics in economics: a philosophically grounded proposal. (English) Zbl 1398.00036 Found. Sci. 22, No. 4, 677-693 (2017). MSC: 00A30 91B02 PDF BibTeX XML Cite \textit{R. Crespo} and \textit{F. Tohmé}, Found. Sci. 22, No. 4, 677--693 (2017; Zbl 1398.00036) Full Text: DOI OpenURL
Pezlar, Ivo Algorithmic theories of problems. A constructive and a non-constructive approach. (English) Zbl 1417.03124 Log. Log. Philos. 26, No. 4, 473-508 (2017). MSC: 03B15 03B60 03F50 03A05 PDF BibTeX XML Cite \textit{I. Pezlar}, Log. Log. Philos. 26, No. 4, 473--508 (2017; Zbl 1417.03124) Full Text: DOI OpenURL
Awodey, Steve Carnap and the invariance of logical truth. (English) Zbl 1417.03003 Synthese 194, No. 1, 67-78 (2017). MSC: 03-03 03A05 01A60 PDF BibTeX XML Cite \textit{S. Awodey}, Synthese 194, No. 1, 67--78 (2017; Zbl 1417.03003) Full Text: DOI OpenURL
Carette, Jacques; Farmer, William M. Formalizing mathematical knowledge as a biform theory graph: a case study. (English) Zbl 1367.68299 Geuvers, Herman (ed.) et al., Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-62074-9/pbk; 978-3-319-62075-6/ebook). Lecture Notes in Computer Science 10383. Lecture Notes in Artificial Intelligence, 9-24 (2017). MSC: 68T30 03B15 03B35 03F30 68T15 PDF BibTeX XML Cite \textit{J. Carette} and \textit{W. M. Farmer}, Lect. Notes Comput. Sci. 10383, 9--24 (2017; Zbl 1367.68299) Full Text: DOI arXiv OpenURL
de Paiva, Valeria; Ritter, Eike Fibrational modal type theory. (English) Zbl 1394.03037 Benevides, Mario (ed.) et al., Proceedings of the 10th workshop on logical and semantic frameworks, with applications (LSFA 2015), Natal, Brazil, August 31 – September 1, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 323, 143-161 (2016). MSC: 03B45 03B70 03G30 PDF BibTeX XML Cite \textit{V. de Paiva} and \textit{E. Ritter}, Electron. Notes Theor. Comput. Sci. 323, 143--161 (2016; Zbl 1394.03037) Full Text: DOI OpenURL
Chatzikyriakidis, Stergios; Luo, Zhaohui Proof assistants for natural language semantics. (English) Zbl 1483.68456 Amblard, Maxime (ed.) et al., Logical aspects of computational linguistics. Celebrating 20 years of LACL (1996–2016). 9th international conference, LACL 2016, Nancy, France, December 5–7, 2016. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 10054, 85-98 (2016). MSC: 68T50 68V15 PDF BibTeX XML Cite \textit{S. Chatzikyriakidis} and \textit{Z. Luo}, Lect. Notes Comput. Sci. 10054, 85--98 (2016; Zbl 1483.68456) Full Text: DOI OpenURL
Rosolini, Giuseppe The category of equilogical spaces and the effective topos as homotopical quotients. (English) Zbl 1375.18018 J. Homotopy Relat. Struct. 11, No. 4, 943-956 (2016). MSC: 18B25 18A15 03B40 03G30 PDF BibTeX XML Cite \textit{G. Rosolini}, J. Homotopy Relat. Struct. 11, No. 4, 943--956 (2016; Zbl 1375.18018) Full Text: DOI arXiv OpenURL
Rahli, Vincent Exercising Nuprl’s open-endedness. (English) Zbl 1434.68644 Greuel, Gert-Martin (ed.) et al., Mathematical software – ICMS 2016. 5th international conference, Berlin, Germany, July 11–14, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9725, 18-27 (2016). MSC: 68V15 03B35 03E25 03F60 68V20 PDF BibTeX XML Cite \textit{V. Rahli}, Lect. Notes Comput. Sci. 9725, 18--27 (2016; Zbl 1434.68644) Full Text: DOI Link OpenURL
Hötzel Escardó, Martín; Streicher, Thomas The intrinsic topology of Martin-Löf universes. (English) Zbl 1402.03022 Ann. Pure Appl. Logic 167, No. 9, 794-805 (2016). MSC: 03B15 03F50 03C90 03D65 PDF BibTeX XML Cite \textit{M. Hötzel Escardó} and \textit{T. Streicher}, Ann. Pure Appl. Logic 167, No. 9, 794--805 (2016; Zbl 1402.03022) Full Text: DOI OpenURL
Escardó, Martín; Xu, Chuangjie A constructive manifestation of the Kleene-Kreisel continuous functionals. (English) Zbl 1402.03020 Ann. Pure Appl. Logic 167, No. 9, 770-793 (2016). MSC: 03B15 03F50 03C90 03D65 PDF BibTeX XML Cite \textit{M. Escardó} and \textit{C. Xu}, Ann. Pure Appl. Logic 167, No. 9, 770--793 (2016; Zbl 1402.03020) Full Text: DOI OpenURL
Lumsdaine, Peter LeFanu; Warren, Michael A. The local universes model: an overlooked coherence construction for dependent type theories. (English) Zbl 1354.03101 ACM Trans. Comput. Log. 16, No. 3, Article No. 23, 31 p. (2015). MSC: 03G30 03B40 55U40 PDF BibTeX XML Cite \textit{P. L. Lumsdaine} and \textit{M. A. Warren}, ACM Trans. Comput. Log. 16, No. 3, Article No. 23, 31 p. (2015; Zbl 1354.03101) Full Text: DOI arXiv OpenURL
Heunen, Chris; Karvonen, Martti Reversible monadic computing. (English) Zbl 1351.68100 Ghica, Dan (ed.), Proceedings of the 31st conference on the mathematical foundations of programming semantics (MFPS XXXI), Nijmegen, The Netherlands, June 22–25, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 319, 217-237, electronic only (2015). MSC: 68Q05 18C20 18C50 18D15 81P15 81P68 PDF BibTeX XML Cite \textit{C. Heunen} and \textit{M. Karvonen}, Electron. Notes Theor. Comput. Sci. 319, 217--237 (2015; Zbl 1351.68100) Full Text: DOI arXiv OpenURL
Pitts, Andrew M.; Matthiesen, Justus; Derikx, Jasper A dependent type theory with abstractable names. (English) Zbl 1342.68054 Ayala-Rincón, Mauricio (ed.) et al., Proceedings of the 9th workshop on logical and semantic frameworks, with applications (LSFA 2014), Brasilia, Brazil, September 8–9, 2014. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 312, 19-50, electronic only (2015). MSC: 68N18 03B15 68Q55 PDF BibTeX XML Cite \textit{A. M. Pitts} et al., Electron. Notes Theor. Comput. Sci. 312, 19--50 (2015; Zbl 1342.68054) Full Text: DOI OpenURL
Awodey, Steve (ed.); Gambino, Nicola (ed.); Palmgren, Erik (ed.) Introduction – from type theory and homotopy theory to univalent foundations. (English) Zbl 1362.03004 Math. Struct. Comput. Sci. 25, No. 5, 1005-1009 (2015). MSC: 03-06 03B15 03G30 18A15 55U40 00B15 PDF BibTeX XML Cite \textit{S. Awodey} (ed.) et al., Math. Struct. Comput. Sci. 25, No. 5, 1005--1009 (2015; Zbl 1362.03004) Full Text: DOI OpenURL
Talian, Andrew J. On endotrivial modules for Lie superalgebras. (English) Zbl 1393.17019 J. Algebra 433, 1-34 (2015). MSC: 17B10 17B56 17B70 PDF BibTeX XML Cite \textit{A. J. Talian}, J. Algebra 433, 1--34 (2015; Zbl 1393.17019) Full Text: DOI arXiv OpenURL
Garner, Richard Combinatorial structure of type dependency. (English) Zbl 1369.03096 J. Pure Appl. Algebra 219, No. 6, 1885-1914 (2015). MSC: 03B15 03G30 18C10 18C50 PDF BibTeX XML Cite \textit{R. Garner}, J. Pure Appl. Algebra 219, No. 6, 1885--1914 (2015; Zbl 1369.03096) Full Text: DOI arXiv OpenURL
Lasson, Marc Canonicity of weak \(\omega\)-groupoid laws using parametricity theory. (English) Zbl 1337.03016 Jacobs, Bart (ed.) et al., Proceedings of the 30th conference on the mathematical foundations of programming semantics (MFPS XXX), Ithaca, NY, USA, June 12–15, 2014. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 308, 229-244, electronic only (2014). MSC: 03B15 03G30 55U40 PDF BibTeX XML Cite \textit{M. Lasson}, Electron. Notes Theor. Comput. Sci. 308, 229--244 (2014; Zbl 1337.03016) Full Text: DOI OpenURL
Pelayo, Álvaro; Warren, Michael A. Homotopy type theory and Voevodsky’s univalent foundations. (English) Zbl 1432.03019 Bull. Am. Math. Soc., New Ser. 51, No. 4, 597-648 (2014). MSC: 03B38 18N45 03G30 55U40 55U35 68N18 PDF BibTeX XML Cite \textit{Á. Pelayo} and \textit{M. A. Warren}, Bull. Am. Math. Soc., New Ser. 51, No. 4, 597--648 (2014; Zbl 1432.03019) Full Text: DOI arXiv OpenURL