Zamdzhiev, Vladimir Semantics for first-order affine inductive data types via slice categories. (English) Zbl 07314154 Petrişan, Daniela (ed.) et al., Coalgebraic methods in computer science. 15th IFIP WG 1.3 international workshop, CMCS 2020, colocated with ETAPS 2020, Dublin, Ireland, April 25–26, 2020. Proceedings. Cham: Springer (ISBN 978-3-030-57200-6/pbk; 978-3-030-57201-3/ebook). Lecture Notes in Computer Science 12094, 180-200 (2020). MSC: 68Q65 PDF BibTeX XML Cite \textit{V. Zamdzhiev}, Lect. Notes Comput. Sci. 12094, 180--200 (2020; Zbl 07314154) Full Text: DOI
van der Weide, Niels Constructing higher inductive types as groupoid quotients. (English) Zbl 07299523 Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-7104-9). 929-943 (2020). MSC: 03B70 PDF BibTeX XML Cite \textit{N. van der Weide}, in: Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8--11, 2020. New York, NY: Association for Computing Machinery (ACM). 929--943 (2020; Zbl 07299523) Full Text: DOI
Sojakova, Kristina; Doorn, Floris van; Rijke, Egbert Sequential colimits in homotopy type theory. (English) Zbl 07299517 Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-7104-9). 845-858 (2020). MSC: 03B70 PDF BibTeX XML Cite \textit{K. Sojakova} et al., in: Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8--11, 2020. New York, NY: Association for Computing Machinery (ACM). 845--858 (2020; Zbl 07299517) Full Text: DOI
Kovács, András; Kaposi, Ambrus Large and infinitary quotient inductive-inductive types. (English) Zbl 07299502 Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-7104-9). 648-661 (2020). MSC: 03B70 PDF BibTeX XML Cite \textit{A. Kovács} and \textit{A. Kaposi}, in: Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8--11, 2020. New York, NY: Association for Computing Machinery (ACM). 648--661 (2020; Zbl 07299502) Full Text: DOI
Gumerov, R. N.; Lipacheva, E. V. Inductive systems of \(C^\ast\)-algebras over posets: a survey. (English) Zbl 1450.81053 Lobachevskii J. Math. 41, No. 4, 644-654 (2020). MSC: 81T05 46L05 16G20 46L57 06F05 46M40 47L80 PDF BibTeX XML Cite \textit{R. N. Gumerov} and \textit{E. V. Lipacheva}, Lobachevskii J. Math. 41, No. 4, 644--654 (2020; Zbl 1450.81053) Full Text: DOI
Grigoryan, T. A.; Kuznetsova, A. Yu. Blaschke \(C^\ast\)-algebras. (English) Zbl 07267662 Lobachevskii J. Math. 41, No. 4, 631-636 (2020). MSC: 46L05 47L80 PDF BibTeX XML Cite \textit{T. A. Grigoryan} and \textit{A. Yu. Kuznetsova}, Lobachevskii J. Math. 41, No. 4, 631--636 (2020; Zbl 07267662) Full Text: DOI
Péchoux, Romain; Perdrix, Simon; Rennela, Mathys; Zamdzhiev, Vladimir Quantum programming with inductive datatypes: causality and affine type theory. (English) Zbl 1442.68034 Goubault-Larrecq, Jean (ed.) et al., Foundations of software science and computation structures. 23rd international conference, FOSSACS 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12077, 562-581 (2020). MSC: 68N30 68N15 68Q55 81P68 PDF BibTeX XML Cite \textit{R. Péchoux} et al., Lect. Notes Comput. Sci. 12077, 562--581 (2020; Zbl 1442.68034) Full Text: DOI
Fiore, Marcelo P.; Pitts, Andrew M.; Steenkamp, S. C. Constructing infinitary quotient-inductive types. (English) Zbl 07250942 Goubault-Larrecq, Jean (ed.) et al., Foundations of software science and computation structures. 23rd international conference, FOSSACS 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020. Proceedings. Cham: Springer (ISBN 978-3-030-45230-8/pbk; 978-3-030-45231-5/ebook). Lecture Notes in Computer Science 12077, 257-276 (2020). MSC: 68Nxx 68Qxx PDF BibTeX XML Cite \textit{M. P. Fiore} et al., Lect. Notes Comput. Sci. 12077, 257--276 (2020; Zbl 07250942) Full Text: DOI
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 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
Ahrens, Benedikt; Matthes, Ralph; Mörtberg, Anders From signatures to Monads in UniMath. (English) Zbl 07096716 J. Autom. Reasoning 63, No. 2, 285-318 (2019). MSC: 68T15 PDF BibTeX XML Cite \textit{B. Ahrens} et al., J. Autom. Reasoning 63, No. 2, 285--318 (2019; Zbl 07096716) Full Text: DOI
Lipacheva, E. V. Embedding semigroup \(C^\ast\)-algebras into inductive limits. (English) Zbl 1433.46034 Lobachevskii J. Math. 40, No. 5, 667-675 (2019). MSC: 46L05 46M40 47L80 PDF BibTeX XML Cite \textit{E. V. Lipacheva}, Lobachevskii J. Math. 40, No. 5, 667--675 (2019; Zbl 1433.46034) Full Text: DOI
Basold, Henning; Hansen, Helle Hvid Well-definedness and observational equivalence for inductive-coinductive programs. (English) Zbl 1452.68044 J. Log. Comput. 29, No. 4, 419-468 (2019). MSC: 68N30 03B70 18C50 PDF BibTeX XML Cite \textit{H. Basold} and \textit{H. H. Hansen}, J. Log. Comput. 29, No. 4, 419--468 (2019; Zbl 1452.68044) Full Text: DOI
Gumerov, R. N. Inductive limits for systems of Toeplitz algebras. (English) Zbl 1434.46032 Lobachevskii J. Math. 40, No. 4, 469-478 (2019). MSC: 46L05 46M40 47L80 PDF BibTeX XML Cite \textit{R. N. Gumerov}, Lobachevskii J. Math. 40, No. 4, 469--478 (2019; Zbl 1434.46032) Full Text: DOI arXiv
Coquand, Thierry; Huber, Simon; Mörtberg, Anders On higher inductive types in cubical type theory. (English) Zbl 1452.03036 Proceedings of the 2018 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, Oxford, UK, July 9–12, 2018. New York, NY: Association for Computing Machinery (ACM). 255-264 (2018). MSC: 03B38 55U35 PDF BibTeX XML Cite \textit{T. Coquand} et al., in: Proceedings of the 2018 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, Oxford, UK, July 9--12, 2018. New York, NY: Association for Computing Machinery (ACM). 255--264 (2018; Zbl 1452.03036) Full Text: DOI
Awodey, Steve; Frey, Jonas; Speight, Sam Impredicative encodings of (higher) inductive types. (English) Zbl 1452.03030 Proceedings of the 2018 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, Oxford, UK, July 9–12, 2018. New York, NY: Association for Computing Machinery (ACM). 76-85 (2018). MSC: 03B38 55U35 18N40 PDF BibTeX XML Cite \textit{S. Awodey} et al., in: Proceedings of the 2018 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, Oxford, UK, July 9--12, 2018. New York, NY: Association for Computing Machinery (ACM). 76--85 (2018; Zbl 1452.03030) Full Text: DOI
Robbestad Gylterud, Håkon From multisets to sets in homotopy type theory. (English) Zbl 06966189 J. Symb. Log. 83, No. 3, 1132-1146 (2018). MSC: 03B15 PDF BibTeX XML Cite \textit{H. Robbestad Gylterud}, J. Symb. Log. 83, No. 3, 1132--1146 (2018; Zbl 06966189) Full Text: DOI
Gumerov, R. N.; Lipacheva, E. V.; Grigoryan, T. A. On inductive limits for systems of \(C^\ast\)-algebras. (English. Russian original) Zbl 1406.46033 Russ. Math. 62, No. 7, 68-73 (2018); translation from Izv. Vyssh. Uchebn. Zaved., Mat. 2018, No. 7, 79-85 (2018). MSC: 46L05 46M40 47L80 PDF BibTeX XML Cite \textit{R. N. Gumerov} et al., Russ. Math. 62, No. 7, 68--73 (2018; Zbl 1406.46033); translation from Izv. Vyssh. Uchebn. Zaved., Mat. 2018, No. 7, 79--85 (2018) Full Text: DOI
Gumerov, R. N. Limit automorphisms of the \(C^\ast\)-algebras generated by isometric representations for semigroups of rationals. (English. Russian original) Zbl 1401.46037 Sib. Math. J. 59, No. 1, 73-84 (2018); translation from Sib. Mat. Zh. 59, No. 1, 95-109 (2018). MSC: 46L05 46L40 46M10 47L80 PDF BibTeX XML Cite \textit{R. N. Gumerov}, Sib. Math. J. 59, No. 1, 73--84 (2018; Zbl 1401.46037); translation from Sib. Mat. Zh. 59, No. 1, 95--109 (2018) Full Text: DOI
Buchholtz, Ulrik; Rijke, Egbert The real projective spaces in homotopy type theory. (English) Zbl 1452.03033 Proceedings of the 2017 32nd annual ACM/IEEE symposium on logic in computer science, LICS 2017, Reykjavík University, Reykjavík, Iceland, June 20–23, 2017. Piscataway, NJ: IEEE Press. Article No. 86, 8 p. (2017). MSC: 03B38 55U35 55P20 PDF BibTeX XML Cite \textit{U. Buchholtz} and \textit{E. Rijke}, in: Proceedings of the 2017 32nd annual ACM/IEEE symposium on logic in computer science, LICS 2017, Reykjavík University, Reykjavík, Iceland, June 20--23, 2017. Piscataway, NJ: IEEE Press. Article No. 86, 8 p. (2017; Zbl 1452.03033) Full Text: Link
Pavaux, Alice Inductive and functional types in ludics. (English) Zbl 1434.03086 Goranko, Valentin (ed.) et al., 26th EACSL annual conference on computer science logic, CSL 2017, Stockholm, Sweden, August 20–24, 2017. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 82, Article 34, 20 p. (2017). MSC: 03B70 03F52 PDF BibTeX XML Cite \textit{A. Pavaux}, LIPIcs -- Leibniz Int. Proc. Inform. 82, Article 34, 20 p. (2017; Zbl 1434.03086) Full Text: DOI
Zucker, Jeffery Feferman on computability. (English) Zbl 1429.03009 Jäger, Gerhard (ed.) et al., Feferman on foundations. Logic, mathematics, philosophy. Cham: Springer. Outst. Contrib. Log. 13, 23-56 (2017). MSC: 03-03 03D65 03D70 03D75 03D78 01A60 PDF BibTeX XML Cite \textit{J. Zucker}, Outst. Contrib. Log. 13, 23--56 (2017; Zbl 1429.03009) Full Text: DOI
Hovsepyan, K. H.; Tsutsulyan, A. V. \(K\)-groups of some subalgebras of the Toeplitz algebra. (English) Zbl 1392.46056 Proc. Yerevan State Univ., Phys. Math. Sci. 51, No. 3, 224-230 (2017). MSC: 46L80 47L80 PDF BibTeX XML Cite \textit{K. H. Hovsepyan} and \textit{A. V. Tsutsulyan}, Proc. Yerevan State Univ., Phys. Math. Sci. 51, No. 3, 224--230 (2017; Zbl 1392.46056)
Reynolds, Andrew; Blanchette, Jasmin Christian A decision procedure for (co)datatypes in SMT solvers. (English) Zbl 1410.68337 J. Autom. Reasoning 58, No. 3, 341-362 (2017). MSC: 68T15 68Q65 PDF BibTeX XML Cite \textit{A. Reynolds} and \textit{J. C. Blanchette}, J. Autom. Reasoning 58, No. 3, 341--362 (2017; Zbl 1410.68337) Full Text: DOI
Yang, Zhe Existence of solutions of generalized quasi-variational relation problems by the inductive relations and some applications. (English) Zbl 1415.49011 J. Syst. Sci. Complex. 29, No. 1, 219-227 (2016). MSC: 49J40 47H10 47J20 PDF BibTeX XML Cite \textit{Z. Yang}, J. Syst. Sci. Complex. 29, No. 1, 219--227 (2016; Zbl 1415.49011) Full Text: DOI
Kraus, Nicolai Constructions with non-recursive higher inductive types. (English) Zbl 1394.03010 Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5–8, 2016. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4391-6). 595-604 (2016). MSC: 03B15 03G30 55U40 PDF BibTeX XML Cite \textit{N. Kraus}, in: Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5--8, 2016. New York, NY: Association for Computing Machinery (ACM). 595--604 (2016; Zbl 1394.03010) Full Text: DOI
Jaber, Guilhem; Lewertowski, Gabriel; Pédrot, Pierre-Marie; Sozeau, Matthieu; Tabareau, Nicolas The definitional side of the forcing. (English) Zbl 1394.68063 Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5–8, 2016. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4391-6). 367-376 (2016). MSC: 68N18 03B40 03E40 03G30 68N30 68T15 PDF BibTeX XML Cite \textit{G. Jaber} et al., in: Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5--8, 2016. New York, NY: Association for Computing Machinery (ACM). 367--376 (2016; Zbl 1394.68063) Full Text: DOI
Basold, Henning; Geuvers, Herman Type theory based on dependent inductive and coinductive types. (English) Zbl 1394.03007 Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5–8, 2016. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4391-6). 327-336 (2016). MSC: 03B15 03G30 68Q65 PDF BibTeX XML Cite \textit{H. Basold} and \textit{H. Geuvers}, in: Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5--8, 2016. New York, NY: Association for Computing Machinery (ACM). 327--336 (2016; Zbl 1394.03007) Full Text: DOI
Cockx, Jesper; Devriese, Dominique; Piessens, Frank Unifiers as equivalences: proof-relevant unification of dependently typed data. (English) Zbl 1360.68321 Garrigue, Jacques (ed.) et al., Proceedings of the 21st ACM SIGPLAN international conference on functional programming, ICFP ’16, Nara, Japan, September 18–22, 2016. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4219-3). 270-283 (2016). MSC: 68N18 68N30 PDF BibTeX XML Cite \textit{J. Cockx} et al., in: Proceedings of the 21st ACM SIGPLAN international conference on functional programming, ICFP '16, Nara, Japan, September 18--22, 2016. New York, NY: Association for Computing Machinery (ACM). 270--283 (2016; Zbl 1360.68321) Full Text: DOI
Nart, Enric On the equivalence of types. (English. French summary) Zbl 1409.11101 J. Théor. Nombres Bordx. 28, No. 3, 743-771 (2016). MSC: 11S05 13A18 11Y40 PDF BibTeX XML Cite \textit{E. Nart}, J. Théor. Nombres Bordx. 28, No. 3, 743--771 (2016; Zbl 1409.11101) Full Text: DOI arXiv
Altenkirch, Thorsten; Kaposi, Ambrus Type theory in type theory using quotient inductive types. (English) Zbl 1347.68045 Bodik, Rastislav (ed.) et al., Proceedings of the 43rd annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’16, St. Petersburg, FL, USA, January 20–22, 2016. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-3549-2). 18-29 (2016). MSC: 68N18 03B15 03B40 03B70 68N30 PDF BibTeX XML Cite \textit{T. Altenkirch} and \textit{A. Kaposi}, in: Proceedings of the 43rd annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '16, St. Petersburg, FL, USA, January 20--22, 2016. New York, NY: Association for Computing Machinery (ACM). 18--29 (2016; Zbl 1347.68045) Full Text: DOI
Buzyakova, Raushan; Chigogidze, Alex Factorization of bijections onto ordered spaces. (English) Zbl 1330.54035 Topology Appl. 198, 38-46 (2016). Reviewer: K. P. Hart (Delft) MSC: 54F05 06F30 54C99 54F45 PDF BibTeX XML Cite \textit{R. Buzyakova} and \textit{A. Chigogidze}, Topology Appl. 198, 38--46 (2016; Zbl 1330.54035) Full Text: DOI arXiv
Blanqui, Frédéric; Jouannaud, Jean-Pierre; Rubio, Albert The computability path ordering. (English) Zbl 1448.68253 Log. Methods Comput. Sci. 11, No. 4, Paper No. 3, 45 p. (2015). MSC: 68Q42 03B35 03B40 03B70 PDF BibTeX XML Cite \textit{F. Blanqui} et al., Log. Methods Comput. Sci. 11, No. 4, Paper No. 3, 45 p. (2015; Zbl 1448.68253) Full Text: DOI
Kaki, Gowtham; Jagannathan, Suresh A relational framework for higher-order shape analysis. (English) Zbl 1345.68062 Proceedings of the 19th ACM SIGPLAN international conference on functional programming, ICFP ’14, Gothenburg, Sweden, September 1–3, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2873-9). 311-324 (2014). MSC: 68N18 68N30 PDF BibTeX XML Cite \textit{G. Kaki} and \textit{S. Jagannathan}, in: Proceedings of the 19th ACM SIGPLAN international conference on functional programming, ICFP '14, Gothenburg, Sweden, September 1--3, 2014. New York, NY: Association for Computing Machinery (ACM). 311--324 (2014; Zbl 1345.68062) Full Text: DOI
Leivant, Daniel M. Global semantic typing for inductive and coinductive computing. (English) Zbl 1356.03073 Log. Methods Comput. Sci. 10, No. 4, Paper No. 18, 23 p. (2014). MSC: 03B70 68N30 PDF BibTeX XML Cite \textit{D. M. Leivant}, Log. Methods Comput. Sci. 10, No. 4, Paper No. 18, 23 p. (2014; Zbl 1356.03073) Full Text: DOI
Dagand, Pierre-Évariste; McBride, Conor A categorical treatment of ornaments. (English) Zbl 1366.68021 Proceedings of the 2013 28th annual ACM/IEEE symposium on logic in computer science, LICS 2013, Tulane University, New Orleans, LA, USA, June 25–28, 2013. Los Alamitos, CA: IEEE Computer Society (ISBN 978-0-7695-5020-6). 530-539 (2013). MSC: 68N30 03B70 68Q65 PDF BibTeX XML Cite \textit{P.-É. Dagand} and \textit{C. McBride}, in: Proceedings of the 2013 28th annual ACM/IEEE symposium on logic in computer science, LICS 2013, Tulane University, New Orleans, LA, USA, June 25--28, 2013. Los Alamitos, CA: IEEE Computer Society. 530--539 (2013; Zbl 1366.68021) Full Text: DOI
Leivant, Daniel Global semantic typing for inductive and coinductive computing. (English) Zbl 1356.03072 Ronchi della Rocca, Simona (ed.), Computer science logic 2013. Selected papers of the 27th CSL workshop and 22nd annual conference of the European Association for Computer Science Logic (EACSL), Torino, Italy, September 2–5, 2013. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-60-6). LIPIcs – Leibniz International Proceedings in Informatics 23, 469-483 (2013). MSC: 03B70 68N30 PDF BibTeX XML Cite \textit{D. Leivant}, LIPIcs -- Leibniz Int. Proc. Inform. 23, 469--483 (2013; Zbl 1356.03072) Full Text: DOI
Fortier, Jérôme; Santocanale, Luigi Cuts for circular proofs: semantics and cut-elimination. (English) Zbl 1356.03098 Ronchi della Rocca, Simona (ed.), Computer science logic 2013. Selected papers of the 27th CSL workshop and 22nd annual conference of the European Association for Computer Science Logic (EACSL), Torino, Italy, September 2–5, 2013. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-60-6). LIPIcs – Leibniz International Proceedings in Informatics 23, 248-262 (2013). MSC: 03F03 03F05 03F07 03G30 PDF BibTeX XML Cite \textit{J. Fortier} and \textit{L. Santocanale}, LIPIcs -- Leibniz Int. Proc. Inform. 23, 248--262 (2013; Zbl 1356.03098) Full Text: DOI
Clairambault, Pierre Strong functors and interleaving fixpoints in game semantics. (English) Zbl 1302.03072 RAIRO, Theor. Inform. Appl. 47, No. 1, 25-68 (2013). Reviewer: Răzvan Diaconescu (Ploiesti) MSC: 03F05 03G30 18C10 PDF BibTeX XML Cite \textit{P. Clairambault}, RAIRO, Theor. Inform. Appl. 47, No. 1, 25--68 (2013; Zbl 1302.03072) Full Text: DOI
van den Berg, Benno Non-deterministic inductive definitions. (English) Zbl 1403.03111 Arch. Math. Logic 52, No. 1-2, 113-135 (2013). MSC: 03E70 03F65 18B30 PDF BibTeX XML Cite \textit{B. van den Berg}, Arch. Math. Logic 52, No. 1--2, 113--135 (2013; Zbl 1403.03111) Full Text: DOI arXiv
Atkey, Robert; Johann, Patricia; Ghani, Neil Refining inductive types. (English) Zbl 1241.68045 Log. Methods Comput. Sci. 8, No. 2, Paper No. 9, 30 p. (2012). MSC: 68N18 68N30 PDF BibTeX XML Cite \textit{R. Atkey} et al., Log. Methods Comput. Sci. 8, No. 2, Paper No. 9, 30 p. (2012; Zbl 1241.68045) Full Text: DOI
Zhou, Chunlai Intuitive probability logic. (English) Zbl 1258.03025 Ogihara, Mitsunori (ed.) et al., Theory and applications of models of computation. 8th annual conference, TAMC 2011, Tokyo, Japan, May 23–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-20876-8/pbk). Lecture Notes in Computer Science 6648, 240-251 (2011). MSC: 03B48 03B45 PDF BibTeX XML Cite \textit{C. Zhou}, Lect. Notes Comput. Sci. 6648, 240--251 (2011; Zbl 1258.03025) Full Text: DOI
Pacheco, Hugo; Cunha, Alcino Generic point-free lenses. (English) Zbl 1286.68099 Bolduc, Claude (ed.) et al., Mathematics of program construction. 10th international conference, MPC 2010, Québec City, Canada, June 21–23, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-13320-6/pbk). Lecture Notes in Computer Science 6120, 331-352 (2010). MSC: 68P01 68N30 PDF BibTeX XML Cite \textit{H. Pacheco} and \textit{A. Cunha}, Lect. Notes Comput. Sci. 6120, 331--352 (2010; Zbl 1286.68099) Full Text: DOI
Miranda-Perea, Favio Ezequiel Some remarks on type systems for course-of-value recursion. (English) Zbl 1310.68055 Horizonte, Belo (ed.) et al., Proceedings of the 3rd workshop on logical and semantic frameworks, with applications (LSFA 2008), Salvador, Brazil, August 26, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 247, 103-121 (2009). MSC: 68N18 68Q55 68Q65 PDF BibTeX XML Cite \textit{F. E. Miranda-Perea}, Electron. Notes Theor. Comput. Sci. 247, 103--121 (2009; Zbl 1310.68055) Full Text: DOI
Miranda-Perea, Favio Ezequiel Two extensions of System F with (co)iteration and primitive (co)recursion principles. (English) Zbl 1197.03013 Theor. Inform. Appl. 43, No. 4, 703-766 (2009). MSC: 03B40 68N18 68N30 68Q65 PDF BibTeX XML Cite \textit{F. E. Miranda-Perea}, Theor. Inform. Appl. 43, No. 4, 703--766 (2009; Zbl 1197.03013) Full Text: DOI EuDML
Aehlig, Klaus Parameter-free polymorphic types. (English) Zbl 1156.03012 Ann. Pure Appl. Logic 156, No. 1, 3-12 (2008). Reviewer: Martin W. Bunder (Wollongong) MSC: 03B40 03F35 PDF BibTeX XML Cite \textit{K. Aehlig}, Ann. Pure Appl. Logic 156, No. 1, 3--12 (2008; Zbl 1156.03012) Full Text: DOI
Abel, Andreas Semi-continuous sized types and termination. (English) Zbl 1143.68013 Log. Methods Comput. Sci. 4, No. 2, Paper 3, 33 p. (2008). MSC: 68N30 68N18 PDF BibTeX XML Cite \textit{A. Abel}, Log. Methods Comput. Sci. 4, No. 2, Paper 3, 33 p. (2008; Zbl 1143.68013) Full Text: DOI
Barrett, Clack; Shikanian, Igor; Tinelli, Cesare An abstract decision procedure for a theory of inductive data types. (English) Zbl 1129.68022 J. Satisf. Boolean Model. Comput. 3, No. 1-2, 21-46 (2007). MSC: 68N18 68N30 68Q65 PDF BibTeX XML Cite \textit{C. Barrett} et al., J. Satisf. Boolean Model. Comput. 3, No. 1--2, 21--46 (2007; Zbl 1129.68022)
Hym, Samuel; Hennessy, Matthew Adding recursion to Dpi. (English) Zbl 1111.68083 Theor. Comput. Sci. 373, No. 3, 182-212 (2007). MSC: 68Q85 PDF BibTeX XML Cite \textit{S. Hym} and \textit{M. Hennessy}, Theor. Comput. Sci. 373, No. 3, 182--212 (2007; Zbl 1111.68083) Full Text: DOI
Danielsson, Nils Anders; Hughes, John; Jansson, Patrik; Gibbons, Jeremy Fast and loose reasoning is morally correct. (English) Zbl 1370.68042 Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’06, Charleston, SC, USA, January 11–13, 2006. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-59593-027-2). 206-217 (2006). MSC: 68N15 68N30 PDF BibTeX XML Cite \textit{N. A. Danielsson} et al., in: Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '06, Charleston, SC, USA, January 11--13, 2006. New York, NY: Association for Computing Machinery (ACM). 206--217 (2006; Zbl 1370.68042) Full Text: DOI
Pitts, Andrew M. Alpha-structural recursion and induction. (English) Zbl 1326.68180 J. ACM 53, No. 3, 459-506 (2006). MSC: 68Q55 03D70 68N15 68Q60 68Q65 PDF BibTeX XML Cite \textit{A. M. Pitts}, J. ACM 53, No. 3, 459--506 (2006; Zbl 1326.68180) Full Text: DOI
Chemouil, David Isomorphisms of simple inductive types through extensional rewriting. (English) Zbl 1096.03009 Math. Struct. Comput. Sci. 15, No. 5, 875-915 (2005). MSC: 03B40 03B70 68N18 PDF BibTeX XML Cite \textit{D. Chemouil}, Math. Struct. Comput. Sci. 15, No. 5, 875--915 (2005; Zbl 1096.03009) Full Text: DOI
Blanqui, Frédéric Inductive types in the calculus of algebraic constructions. (English) Zbl 1094.03018 Fundam. Inform. 65, No. 1-2, 61-86 (2005). Reviewer: Manuel Ojeda Aciego (Málaga) MSC: 03B70 03B40 68Q42 03B35 PDF BibTeX XML Cite \textit{F. Blanqui}, Fundam. Inform. 65, No. 1--2, 61--86 (2005; Zbl 1094.03018)
Luo, Zhaohui; Luo, Yong Transitivity in coercive subtyping. (English) Zbl 1064.03021 Inf. Comput. 197, No. 1-2, 122-144 (2005). MSC: 03B70 03F35 03B35 PDF BibTeX XML Cite \textit{Z. Luo} and \textit{Y. Luo}, Inf. Comput. 197, No. 1--2, 122--144 (2005; Zbl 1064.03021) Full Text: DOI
Vouillon, Jerome; Melliès, Paul-André Semantic types: a fresh look at the ideal model for types. (English) Zbl 1325.68072 Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’04, Venice, Italy, January 14–16, 2004. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-58113-729-X). 52-63 (2004). MSC: 68N30 68Q55 PDF BibTeX XML Cite \textit{J. Vouillon} and \textit{P.-A. Melliès}, in: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '04, Venice, Italy, January 14--16, 2004. New York, NY: Association for Computing Machinery (ACM). 52--63 (2004; Zbl 1325.68072) Full Text: DOI
Abel, Andreas Termination checking with types. (English) Zbl 1089.68028 Theor. Inform. Appl. 38, No. 4, 277-319 (2004). MSC: 68N18 68Q42 PDF BibTeX XML Cite \textit{A. Abel}, Theor. Inform. Appl. 38, No. 4, 277--319 (2004; Zbl 1089.68028) Full Text: DOI Numdam EuDML
Barthe, G.; Frade, M. J.; Giménez, E.; Pinto, L.; Uustalu, T. Type-based termination of recursive definitions. (English) Zbl 1054.68027 Math. Struct. Comput. Sci. 14, No. 1, 97-141 (2004). Reviewer: Neculai Curteanu (Iaşi) MSC: 68N18 03B40 03B70 68Q65 68Q60 68Q55 68T15 PDF BibTeX XML Cite \textit{G. Barthe} et al., Math. Struct. Comput. Sci. 14, No. 1, 97--141 (2004; Zbl 1054.68027) Full Text: DOI
Dybjer, Peter; Setzer, Anton Induction-recursion and initial algebras. (English) Zbl 1044.03021 Ann. Pure Appl. Logic 124, No. 1-3, 1-47 (2003). Reviewer: Raymond Turner (Essex) MSC: 03B70 03F35 03F50 18C50 68Q65 03E55 PDF BibTeX XML Cite \textit{P. Dybjer} and \textit{A. Setzer}, Ann. Pure Appl. Logic 124, No. 1--3, 1--47 (2003; Zbl 1044.03021) Full Text: DOI
Matthes, Ralph Tarski’s fixed-point theorem and lambda calculi with monotone inductive types. (English) Zbl 1069.03009 Synthese 133, No. 1-2, 107-129 (2002). MSC: 03B40 18C50 68N18 PDF BibTeX XML Cite \textit{R. Matthes}, Synthese 133, No. 1--2, 107--129 (2002; Zbl 1069.03009) Full Text: DOI
Santocanale, Luigi \(\mu\)-bicomplete categories and parity games. (English) Zbl 1024.18001 Theor. Inform. Appl. 36, No. 2, 195-227 (2002). Reviewer: Václav Koubek (Praha) MSC: 18A30 68Q65 91A43 18B05 18C50 PDF BibTeX XML Cite \textit{L. Santocanale}, Theor. Inform. Appl. 36, No. 2, 195--227 (2002; Zbl 1024.18001) Full Text: DOI Numdam EuDML
Pollack, Robert Dependently typed records in type theory. (English) Zbl 1001.68013 Formal Asp. Comput. 13, No. 3-5, 386-402 (2002). MSC: 68N15 68P05 PDF BibTeX XML Cite \textit{R. Pollack}, Formal Asp. Comput. 13, No. 3--5, 386--402 (2002; Zbl 1001.68013) Full Text: DOI
Clausing, Thorsten A syntactic framework with probabilistic beliefs and conditionals for the analysis of strategic form games. (English) Zbl 1006.03019 J. Logic Lang. Inf. 11, No. 3, 335-348 (2002). Reviewer: Giacomo Bonanno (Davis) MSC: 03B48 91A10 03B42 91B52 PDF BibTeX XML Cite \textit{T. Clausing}, J. Logic Lang. Inf. 11, No. 3, 335--348 (2002; Zbl 1006.03019) Full Text: DOI
Uustalu, Tarmo; Vene, Varmo Least and greatest fixed points in intuitionistic natural deduction. (English) Zbl 0984.68136 Theor. Comput. Sci. 272, No. 1-2, 315-339 (2002). MSC: 68T15 PDF BibTeX XML Cite \textit{T. Uustalu} and \textit{V. Vene}, Theor. Comput. Sci. 272, No. 1--2, 315--339 (2002; Zbl 0984.68136) Full Text: DOI
Blanqui, Frédéric; Jouannaud, Jean-Pierre; Okada, Mitsuhiro Inductive-data-type systems. (English) Zbl 0992.68121 Theor. Comput. Sci. 272, No. 1-2, 41-68 (2002); corrigendum ibid. 817, 81-82 (2020). MSC: 68Q42 68N18 68Q65 PDF BibTeX XML Cite \textit{F. Blanqui} et al., Theor. Comput. Sci. 272, No. 1--2, 41--68 (2002; Zbl 0992.68121) Full Text: DOI
Fu, Yuxi Semantics of constructions. II: The initial algebraic approach. (English) Zbl 0992.68139 J. Comput. Sci. Technol. 16, No. 2, 137-145 (2001). MSC: 68Q55 PDF BibTeX XML Cite \textit{Y. Fu}, J. Comput. Sci. Technol. 16, No. 2, 137--145 (2001; Zbl 0992.68139) Full Text: DOI
Fu, Yuxi Semantics of constructions. I: The traditional approach. (English) Zbl 0974.03032 J. Comput. Sci. Technol. 16, No. 1, 13-24 (2001). MSC: 03B70 68Q55 03F35 PDF BibTeX XML Cite \textit{Y. Fu}, J. Comput. Sci. Technol. 16, No. 1, 13--24 (2001; Zbl 0974.03032) Full Text: DOI
Comon, Hubert; Nieuwenhuis, Robert Induction = I-axiomatization + first-order consistency. (English) Zbl 1046.68640 Inf. Comput. 159, No. 1-2, 151-186 (2000). MSC: 68T15 68Q65 03B35 68Q42 PDF BibTeX XML Cite \textit{H. Comon} and \textit{R. Nieuwenhuis}, Inf. Comput. 159, No. 1--2, 151--186 (2000; Zbl 1046.68640) Full Text: DOI
Callaghan, Paul; Luo, Zhaohui Implementation techniques for inductive types in Plastic. (English) Zbl 0988.68053 Coquand, Thierry (ed.) et al., Types for proofs and programs. 3rd international workshop, TYPES ’99, Lökeberg, Sweden, June 12-16, 1999. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1956, 94-113 (2000). MSC: 68N30 03B70 PDF BibTeX XML Cite \textit{P. Callaghan} and \textit{Z. Luo}, Lect. Notes Comput. Sci. 1956, 94--113 (2000; Zbl 0988.68053)
Schmets, Jean; Valdivia, Manuel Extension maps in ultradifferentiable and ultraholomorphic function spaces. (English) Zbl 0972.46013 Stud. Math. 143, No. 3, 221-250 (2000). Reviewer: Klaus Dieter Bierstedt (Paderborn) MSC: 46E10 46F05 30D60 46A13 30H05 46A04 46A45 PDF BibTeX XML Cite \textit{J. Schmets} and \textit{M. Valdivia}, Stud. Math. 143, No. 3, 221--250 (2000; Zbl 0972.46013) Full Text: DOI EuDML
Puitg, F.; Dufourd, J.-F. Formalizing mathematics in higher-order logic: A case study in geometric modelling. (English) Zbl 0945.68178 Theor. Comput. Sci. 234, No. 1-2, 1-57 (2000). MSC: 68U05 68Q65 PDF BibTeX XML Cite \textit{F. Puitg} and \textit{J. F. Dufourd}, Theor. Comput. Sci. 234, No. 1--2, 1--57 (2000; Zbl 0945.68178) Full Text: DOI
Bouhoula, A.; Jouannaud, J.-P.; Meseguer, J. Specification and proof in membership equational logic. (English) Zbl 0938.68057 Theor. Comput. Sci. 236, No. 1-2, 35-132 (2000). MSC: 68Q65 PDF BibTeX XML Cite \textit{A. Bouhoula} et al., Theor. Comput. Sci. 236, No. 1--2, 35--132 (2000; Zbl 0938.68057) Full Text: DOI
Altenkirch, Thorsten; Reus, Bernhard Monadic presentations of lambda terms using generalized inductive types. (English) Zbl 0944.03011 Flum, Jörg (ed.) et al., Computer science logic. 13th international workshop, CSL ’99. 8th annual conference of the EACSL, Madrid, Spain, September 20-25, 1999. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1683, 453-468 (1999). MSC: 03B40 18C15 03B35 PDF BibTeX XML Cite \textit{T. Altenkirch} and \textit{B. Reus}, Lect. Notes Comput. Sci. 1683, 453--468 (1999; Zbl 0944.03011)
Geuvers, Herman; Poll, Erik; Zwanenburg, Jan Safe proof checking in type theory with \(Y\). (English) Zbl 0944.03008 Flum, Jörg (ed.) et al., Computer science logic. 13th international workshop, CSL ’99. 8th annual conference of the EACSL, Madrid, Spain, September 20-25, 1999. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1683, 439-452 (1999). MSC: 03B35 03B40 PDF BibTeX XML Cite \textit{H. Geuvers} et al., Lect. Notes Comput. Sci. 1683, 439--452 (1999; Zbl 0944.03008)
Matthes, Ralph Monotone (co)inductive types and positive fixed-point types. (English) Zbl 0940.03018 Theor. Inform. Appl. 33, No. 4-5, 309-328 (1999). MSC: 03B40 68Q42 68Q65 PDF BibTeX XML Cite \textit{R. Matthes}, Theor. Inform. Appl. 33, No. 4--5, 309--328 (1999; Zbl 0940.03018) Full Text: DOI EuDML
Uustalu, Tarmo; Vene, Varmo Mendler-style inductive types, categorically. (English) Zbl 0937.68029 Nord. J. Comput. 6, No. 3, 343-361 (1999). MSC: 68N18 68N15 PDF BibTeX XML Cite \textit{T. Uustalu} and \textit{V. Vene}, Nord. J. Comput. 6, No. 3, 343--361 (1999; Zbl 0937.68029)
Barendregt, Henk Problems in type theory. (English) Zbl 0933.03077 Berger, Ulrich (ed.) et al., Computational logic. Proceedings of the NATO ASI, Marktoberdorf, Germany, July 29–August 10, 1997. Berlin: Springer. NATO ASI Ser., Ser. F, Comput. Syst. Sci. 165, 99-111 (1999). MSC: 03F35 03B40 PDF BibTeX XML Cite \textit{H. Barendregt}, NATO ASI Ser., Ser. F, Comput. Syst. Sci. 165, 99--111 (1999; Zbl 0933.03077)
Altenkirch, Thorsten Logical relations and inductive/coinductive types. (English) Zbl 0934.03019 Gottlob, Georg (ed.) et al., Computer science logic. 12th international workshop, CSL ’98, annual conference of the EACSL, Brno, Czech Republic, August 24-28, 1998. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1584, 343-354 (1999). MSC: 03B40 PDF BibTeX XML Cite \textit{T. Altenkirch}, Lect. Notes Comput. Sci. 1584, 343--354 (1999; Zbl 0934.03019)
Stefanova, Milena A schematic proof of strong normalization for the system of the \(\lambda\)-cube. (English) Zbl 1079.03528 God. Sofij. Univ., Fak. Mat. Inform. 90(1996), No. 1, 17-40 (1998). MSC: 03B40 PDF BibTeX XML Cite \textit{M. Stefanova}, God. Sofiĭ. Univ., Fak. Mat. Inform. 90, No. 1, 17--40 (1998; Zbl 1079.03528)
Matthes, Ralph Extensions of system F by iteration and primitive recursion on monotone inductive types. (English) Zbl 0943.68086 München: Utz Verlag. München: LMU, Univ. München, Fakultät Mathematik/ Informatik, xi, 185 p. (1998). Reviewer: Christian Posthoff (St.Augustine) MSC: 68Q42 68-02 PDF BibTeX XML Cite \textit{R. Matthes}, Extensions of system F by iteration and primitive recursion on monotone inductive types. München: Utz Verlag; München: LMU, Univ. München, Fakultät Mathematik/ Informatik (1998; Zbl 0943.68086)
Hedberg, Michael A coherence theorem for Martin-Löf’s type theory. (English) Zbl 0917.03028 J. Funct. Program. 8, No. 4, 413-436 (1998). MSC: 03F35 03G30 03B40 PDF BibTeX XML Cite \textit{M. Hedberg}, J. Funct. Program. 8, No. 4, 413--436 (1998; Zbl 0917.03028) Full Text: DOI
Aliprantis, C. D.; Brown, D. J.; Polyrakis, I. A.; Werner, J. Yudin cones and inductive limit topologies. (English) Zbl 1053.91511 Atti Semin. Mat. Fis. Univ. Modena 46, No. 2, 389-412 (1998). Reviewer: Dave Furth (MR1665927) MSC: 91B52 46A13 46N10 91B24 PDF BibTeX XML Cite \textit{C. D. Aliprantis} et al., Atti Semin. Mat. Fis. Univ. Modena 46, No. 2, 389--412 (1998; Zbl 1053.91511)
Giménez, Eduardo Structural recursive definitions in type theory. (English) Zbl 0910.03022 Larsen, Kim G. (ed.) et al., Automata, languages and programming. 25th international colloquium, ICALP ’98. Aalborg, Denmark, July 13–17, 1998. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1443, 397-408 (1998). MSC: 03B70 03F35 03B15 PDF BibTeX XML Cite \textit{E. Giménez}, Lect. Notes Comput. Sci. 1443, 397--408 (1998; Zbl 0910.03022)
Avigad, Jeremy; Feferman, Solomon Gödel’s functional (“Dialectica”) interpretation. (English) Zbl 0913.03053 Buss, Samuel R. (ed.), Handbook of proof theory. Amsterdam: Elsevier. Stud. Logic Found. Math. 137, 337-405 (1998). Reviewer: A.Cantini (Firenze) MSC: 03F30 03-02 03F35 03F55 03F50 03F60 PDF BibTeX XML Cite \textit{J. Avigad} and \textit{S. Feferman}, Stud. Logic Found. Math. 137, 337--405 (1998; Zbl 0913.03053)
Amadio, Roberto M.; Coupet-Grimal, Solange Analysis of a guard condition in type theory. (Extended abstract). (English) Zbl 0922.03021 Nivat, Maurice (ed.), Foundations of software science and computation structures. 1st international conference, FoSSaCS ’98. Held as part of the joint European conferences on Theory and practice of software, ETAPS ’98, Lisbon, Portugal, March 28 - April 4, 1998. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1378, 48-62 (1998). Reviewer: Christophe Raffalli MSC: 03B40 03B70 68Q55 PDF BibTeX XML Cite \textit{R. M. Amadio} and \textit{S. Coupet-Grimal}, Lect. Notes Comput. Sci. 1378, 48--62 (1998; Zbl 0922.03021)
Kristiansen, Lill; Normann, Dag Total objects in inductively defined types. (English) Zbl 0881.03026 Arch. Math. Logic 36, No. 6, 405-436 (1997). MSC: 03D65 03F35 PDF BibTeX XML Cite \textit{L. Kristiansen} and \textit{D. Normann}, Arch. Math. Logic 36, No. 6, 405--436 (1997; Zbl 0881.03026) Full Text: DOI
Tan, Qingping A higher-order unification algorithm for inductive types and dependent types. (English) Zbl 0878.68069 J. Comput. Sci. Technol. 12, No. 3, 231-243 (1997). MSC: 68W10 PDF BibTeX XML Cite \textit{Q. Tan}, J. Comput. Sci. Technol. 12, No. 3, 231--243 (1997; Zbl 0878.68069) Full Text: DOI
Loader, Ralph Equational theories for inductive types. (English) Zbl 0873.03019 Ann. Pure Appl. Logic 84, No. 2, 175-217 (1997). MSC: 03B40 03G30 PDF BibTeX XML Cite \textit{R. Loader}, Ann. Pure Appl. Logic 84, No. 2, 175--217 (1997; Zbl 0873.03019) Full Text: DOI
Asperti, Andrea; Laneve, Cosimo Interaction systems II: The practice of optimal reductions. (English) Zbl 0873.03015 Theor. Comput. Sci. 159, No. 2, 191-244 (1996). MSC: 03B40 68Q42 68M10 PDF BibTeX XML Cite \textit{A. Asperti} and \textit{C. Laneve}, Theor. Comput. Sci. 159, No. 2, 191--244 (1996; Zbl 0873.03015) Full Text: DOI
Naumann, David A. A recursion theorem for predicate transformers on inductive data types. (English) Zbl 0823.68063 Inf. Process. Lett. 50, No. 6, 329-336 (1994). MSC: 68Q65 PDF BibTeX XML Cite \textit{D. A. Naumann}, Inf. Process. Lett. 50, No. 6, 329--336 (1994; Zbl 0823.68063) Full Text: DOI
Lugiez, D.; Moysset, J. L. Complement problems and tree automata in AC-like theories. (English) Zbl 0795.68139 Enjalbert, Patrice (ed.) et al., STACS 93. 10th annual symposium on theoretical aspects of computer science, Würzburg, Germany, February 25-27, 1993. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 665, 515-524 (1993). Reviewer: D.Lugiez (Nancy) MSC: 68Q45 68T15 68Q65 68Q42 PDF BibTeX XML Cite \textit{D. Lugiez} and \textit{J. L. Moysset}, Lect. Notes Comput. Sci. 665, 515--524 (1993; Zbl 0795.68139)
Altenkirch, Thorsten A formalization of the strong normalization proof for system F in LEGO. (English) Zbl 0797.68095 Bezem, Marc (ed.) et al., Typed Lambda calculi and applications. International conference, TLCA ’93, March 16-18, 1993, Utrecht, the Netherlands. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 664, 13-28 (1993). MSC: 68Q45 03B40 03B15 PDF BibTeX XML Cite \textit{T. Altenkirch}, Lect. Notes Comput. Sci. 664, 13--28 (1993; Zbl 0797.68095)
Dybkjær, Hans; Melton, Austin Comparing Hagino’s categorical programming language and typed lambda- calculi. (English) Zbl 0787.68014 Theor. Comput. Sci. 111, No. 1-2, 145-189 (1993). MSC: 68N15 03B40 68Q55 08A70 18D15 PDF BibTeX XML Cite \textit{H. Dybkjær} and \textit{A. Melton}, Theor. Comput. Sci. 111, No. 1--2, 145--189 (1993; Zbl 0787.68014) Full Text: DOI
Dowek, Gilles The undecidability of pattern matching in calculi where primitive recursive functions are representable. (English) Zbl 0773.03011 Theor. Comput. Sci. 107, No. 2, 349-356 (1993). MSC: 03B40 03B25 03D20 03D35 PDF BibTeX XML Cite \textit{G. Dowek}, Theor. Comput. Sci. 107, No. 2, 349--356 (1993; Zbl 0773.03011) Full Text: DOI
Ore, Christian-Emil The extended calculus of constructions (ECC) with inductive types. (English) Zbl 0784.03009 Inf. Comput. 99, No. 2, 231-264 (1992). MSC: 03B15 68N15 PDF BibTeX XML Cite \textit{C.-E. Ore}, Inf. Comput. 99, No. 2, 231--264 (1992; Zbl 0784.03009) Full Text: DOI
Barzdins, Guntis Inductive synthesis of term rewriting systems. (English) Zbl 1412.68290 Bārzdiṇš, Jānis (ed.) et al., Baltic computer science. Selected papers. Berlin etc.: Springer-Verlag. Lect. Notes Comput. Sci. 502, 253-285 (1991). MSC: 68W01 68Q32 68Q42 68Q65 PDF BibTeX XML Cite \textit{G. Barzdins}, Lect. Notes Comput. Sci. 502, 253--285 (1991; Zbl 1412.68290) Full Text: DOI
Kapur, Deepak; Narendran, Paliath; Rosenkrantz, Daniel J.; Zhang, Hantao Sufficient-completeness, ground-reducibility and their complexity. (English) Zbl 0721.68032 Acta Inf. 28, No. 4, 311-350 (1991). Reviewer: S.P.Yukna (Vilnius) MSC: 68Q42 68Q65 68Q25 03D15 03D03 PDF BibTeX XML Cite \textit{D. Kapur} et al., Acta Inf. 28, No. 4, 311--350 (1991; Zbl 0721.68032) Full Text: DOI
Hallnäs, Lars Partial inductive definitions. (English) Zbl 0770.68039 Theor. Comput. Sci. 87, No. 1, 115-142 (1991). MSC: 68N17 03B15 03F03 68Q65 68T15 PDF BibTeX XML Cite \textit{L. Hallnäs}, Theor. Comput. Sci. 87, No. 1, 115--142 (1991; Zbl 0770.68039) Full Text: DOI
Amadio, Roberto M. Recursion over realizability structures. (English) Zbl 0760.03012 Inf. Comput. 91, No. 1, 55-85 (1991). Reviewer: M.Eytan (Strasbourg) MSC: 03D80 03B40 68Q55 03F50 18D15 PDF BibTeX XML Cite \textit{R. M. Amadio}, Inf. Comput. 91, No. 1, 55--85 (1991; Zbl 0760.03012) Full Text: DOI
Comon, Hubert Equational formulas in order-sorted algebras. (English) Zbl 0774.68071 Automata, languages and programming, Proc. 17th Int. Colloq., Warwick/GB 1990, Lect. Notes Comput. Sci. 443, 674-688 (1990). MSC: 68Q42 68Q65 68T15 03B25 68Q45 PDF BibTeX XML Cite \textit{H. Comon}, Lect. Notes Comput. Sci. 443, 674--688 (1990; Zbl 0774.68071)
Jouannaud, Jean-Pierre; Kounalis, Emmanuel Automatic proofs by induction in theories without constructors. (English) Zbl 0682.68032 Inf. Comput. 82, No. 1, 1-33 (1989). MSC: 68W30 68T15 03D03 68Q65 PDF BibTeX XML Cite \textit{J.-P. Jouannaud} and \textit{E. Kounalis}, Inf. Comput. 82, No. 1, 1--33 (1989; Zbl 0682.68032) Full Text: DOI
Jäger, Gerhard Non-monotonic reasoning by axiomatic extensions. (English) Zbl 0681.03012 Logic, methodology and philosophy of science VIII, Proc. 8th Int. Congr., Moscow/USSR 1987, Stud. Logic Found. Math. 126, 93-110 (1989). Reviewer: D.Makinson MSC: 03B60 03D70 68Q65 PDF BibTeX XML