Xue, Tao; Luo, Zhaohui; Chatzikyriakidis, Stergios Propositional forms of judgemental interpretations. (English) Zbl 1540.03031 J. Logic Lang. Inf. 32, No. 4, 733-758 (2023). Reviewer: Serguei V. Solov’ev (Toulouse) MSC: 03B38 03B65 × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF Full Text: DOI Link
Pollack, Randy; Sato, Masahiko; Ricciotti, Wilmer A canonical locally named representation of binding. (English) Zbl 1270.68073 J. Autom. Reasoning 49, No. 2, 185-207 (2012). MSC: 68N18 03B40 68T15 × Cite Format Result Cite Review PDF Full Text: DOI
Charguéraud, Arthur The locally nameless representation. (English) Zbl 1260.68368 J. Autom. Reasoning 49, No. 3, 363-408 (2012). MSC: 68T15 68N15 68N18 × Cite Format Result Cite Review PDF Full Text: DOI
Felty, Amy; Momigliano, Alberto Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax. (English) Zbl 1252.68252 J. Autom. Reasoning 48, No. 1, 43-105 (2012). MSC: 68T15 03B70 × Cite Format Result Cite Review PDF Full Text: DOI
Abel, Andreas; Altenkirch, Thorsten A partial type checking algorithm for Type:Type. (English) Zbl 1291.68106 Capretta, Venanzio (ed.) et al., Proceedings of the second workshop on mathematically structured functional programming (MSFP 2008), Reykjavik, Iceland, July 6, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 229, No. 5, 3-17 (2011). MSC: 68N18 68N30 × Cite Format Result Cite Review PDF Full Text: DOI
Sozeau, Matthieu Equations: a dependent pattern-matching compiler. (English) Zbl 1291.68369 Kaufmann, Matt (ed.) et al., Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14051-8/pbk). Lecture Notes in Computer Science 6172, 419-434 (2010). MSC: 68T15 68N20 × Cite Format Result Cite Review PDF Full Text: DOI
Chapman, James Type theory should eat itself. (English) Zbl 1337.68057 Abel, Andreas (ed.) et al., Proceedings of the 3rd international workshop on logical frameworks and metalanguages: theory and practice (LFMTP 2008), Pittsburgh, PA, USA, June 23, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 228, 21-36 (2009). MSC: 68N18 68N15 68N30 × Cite Format Result Cite Review PDF Full Text: DOI
Asperti, A.; Ricciotti, W.; Sacerdoti Coen, C.; Tassi, E. A compact kernel for the calculus of inductive constructions. (English) Zbl 1196.68221 Sādhanā 34, No. 1, 71-144 (2009). MSC: 68T15 × Cite Format Result Cite Review PDF Full Text: DOI Link
Nanevski, Aleksandar; Morrisett, Greg; Shinnar, Avraham; Govereau, Paul; Birkedal, Lars Ynot: dependent types for imperative programs. (English) Zbl 1323.68142 Proceedings of the 13th ACM SIGPLAN international conference on functional programming, ICFP ’08, Victoria, BC, Canada, September 20–28, 2008. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-59593-919-7). ACM SIGPLAN Notices 43, No. 9, 229-240 (2008). MSC: 68N18 03B70 68N15 68T15 × Cite Format Result Cite Review PDF Full Text: DOI
Luo, Zhaohui; Adams, Robin Structural subtyping for inductive types with functorial equality rules. (English) Zbl 1156.68017 Math. Struct. Comput. Sci. 18, No. 5, 931-972 (2008). MSC: 68N30 × Cite Format Result Cite Review PDF Full Text: DOI
Sheard, Tim Type-level computation using narrowing in \(\Omega\)mega. (English) Zbl 1277.68046 Stump, Aron (ed.) et al., Proceedings of the programming languages meets program verification (PLPV 2006), Seattle, WA, USA, August 21, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 174, No. 7, 105-128 (2007). MSC: 68N15 03B70 68N18 68T15 × Cite Format Result Cite Review PDF Full Text: DOI
Brady, Edwin Ivor, a proof engine. (English) Zbl 1226.68094 Horváth, Zoltán (ed.) et al., Implementation and application of functional languages. 18th international symposium, IFL 2006, Budapest, Hungary, September 4–6, 2006. Revised selected papers. Berlin: Springer (ISBN 978-3-540-74129-9/pbk). Lecture Notes in Computer Science 4449, 145-162 (2007). MSC: 68T15 68N18 × Cite Format Result Cite Review PDF Full Text: DOI
Brady, Edwin; Hammond, Kevin A dependently typed framework for static analysis of program execution costs. (English) Zbl 1236.68045 Butterfield, Andrew (ed.) et al., Implementation and application of functional languages. 17th international workshop, IFL 2005, Dublin, Ireland, September 19–21, 2005. Revised selected papers. Berlin: Springer (ISBN 978-3-540-69174-7/pbk). Lecture Notes in Computer Science 4015, 74-90 (2006). MSC: 68N30 68N18 × Cite Format Result Cite Review PDF Full Text: DOI
Morris, Peter; Altenkirch, Thorsten; McBride, Conor Exploring the regular tree types. (English) Zbl 1172.68401 Filliâtre, Jean-Christophe (ed.) et al., Types for proofs and programs. International workshop, TYPES 2004, Jouy-en-Josas, France, December 15–18, 2004. Revised selected papers. Berlin: Springer (ISBN 3-540-31428-8/pbk). Lecture Notes in Computer Science 3839, 252-267 (2006). MSC: 68N18 68N30 × Cite Format Result Cite Review PDF Full Text: DOI
Westbrook, Edwin; Stump, Aaron; Wehrman, Ian A language-based approach to functionally correct imperative programming. (English) Zbl 1302.68095 Proceedings of the 10th ACM SIGPLAN international conference on functional programming, ICFP ’05, Tallinn, Estonia, September 26–28, 2005. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-59593-064-7). ACM SIGPLAN Notices 40, No. 9, 268-279 (2005). MSC: 68N30 × Cite Format Result Cite Review PDF Full Text: DOI Link
Delahaye, David; Mayero, Micaela Dealing with algebraic expressions over a field in Coq using Maple. (English) Zbl 1126.68101 J. Symb. Comput. 39, No. 5, 569-592 (2005). MSC: 68W30 68T15 × Cite Format Result Cite Review PDF Full Text: DOI
McBride, Conor Epigram: Practical programming with dependent types. (English) Zbl 1158.68356 Vene, Varmo (ed.) et al., Advanced functional programming. 5th international school, AFP 2004, Tartu, Estonia, August 14–21, 2004. Revised lectures. Berlin: Springer (ISBN 3-540-28540-7/pbk). Lecture Notes in Computer Science 3622, 130-170 (2005). MSC: 68N18 × Cite Format Result Cite Review PDF Full Text: DOI
Schürmann, Carsten Twelf and Delphin: logic and functional programming in a meta-logical framework. (English) Zbl 1122.68391 Kameyama, Yukiyoshi (ed.) et al., Functional and logic programming. 7th international symposium, FLOPS 2004, Nara, Japan, April 7–9, 2004. Proceedings. Berlin: Springer (ISBN 3-540-21402-X/pbk). Lecture Notes in Computer Science 2998, 22-23 (2004). MSC: 68N17 68N18 × Cite Format Result Cite Review PDF Full Text: DOI
Kutsia, Temur; Buchberger, Bruno Predicate logic with sequence variables and sequence function symbols. (English) Zbl 1109.68111 Asperti, Andrea (ed.) et al., Mathematical knowledge management. Third international conference, MKM 2004, Białowieża, Poland, September 19–21, 2004. Proceedings. Berlin: Springer (ISBN 3-540-23029-7/pbk). Lecture Notes in Computer Science 3119, 205-219 (2004). MSC: 68T30 03B10 03B70 68T15 × Cite Format Result Cite Review PDF Full Text: DOI
Buchberger, Bruno Algorithm-supported mathematical theory exploration: A personal view and strategy. (English) Zbl 1109.68664 Buchberger, Bruno (ed.) et al., Artificial intelligence and symbolic computation. 7th international conference, AISC 2004, Linz, Austria, September 22–24, 2004. Proceedings. Berlin: Springer (ISBN 3-540-23212-5/pbk). Lecture Notes in Computer Science 3249. Lecture Notes in Artificial Intelligence, 236-250 (2004). MSC: 68T99 68W30 68T15 × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF Full Text: DOI Numdam EuDML Link
Bertot, Yves; Castéran, Pierre Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. (English) Zbl 1069.68095 Texts in Theoretical Computer Science. An EATCS Series. Berlin: Springer (ISBN 3-540-20854-2/hbk). xxv, 469 p. (2004). Reviewer: Valentin F. Goranko (Johannesburg) MSC: 68T15 03B15 03B35 03B70 68N18 68Q60 68-01 × Cite Format Result Cite Review PDF
Bruni, Roberto; Honsell, Furio; Lenisa, Marina; Miculan, Marino Comparing higher-order encodings in logical frameworks and tile logic. (English) Zbl 1268.68047 Lenisa, Mariana (ed.) et al., TOSCA 2001. Proceedings of the workshop on theory of concurrency, higher order languages and types, Udine, Italy, November 19–21, 2001. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 62, 136-156 (2002). MSC: 68N18 03B70 × Cite Format Result Cite Review PDF Full Text: DOI
McBride, Conor Elimination with a motive. (English) Zbl 1054.03501 Callaghan, Paul (ed.) et al., Types for proofs and programs. International workshop, TYPES 2000, Durham, GB, December 8–12, 2000. Selected papers. Berlin: Springer (ISBN 3-540-43287-6). Lect. Notes Comput. Sci. 2277, 197-216 (2002). MSC: 03B35 68T15 × Cite Format Result Cite Review PDF Full Text: Link
Barthe, Gilles; Courtieu, Pierre Efficient reasoning about executable specifications in Coq. (English) Zbl 1013.68539 Carreño, Victor A. (ed.) et al., Theorem proving in higher order logics. 15th international conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2410, 31-46 (2002). MSC: 68T15 03B35 × Cite Format Result Cite Review PDF Full Text: Link
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 × Cite Format Result Cite Review PDF Full Text: DOI
McBride, Conor Faking it simulating dependent types in Haskell. (English) Zbl 1037.68038 J. Funct. Program. 12, No. 4-5, 375-392 (2002). MSC: 68N18 68P05 × Cite Format Result Cite Review PDF Full Text: DOI
Taha, Walid; Hudak, Paul; Wan, Zhanyong Directions in functional programming for real(-time) applications. (English) Zbl 1050.68514 Henzinger, Thomas A. (ed.) et al., Embedded software. 1st international workshop, EMSOFT 2001, Tahoe City, CA, USA, October 8–10, 2001. Proceedings. Berlin: Springer (ISBN 3-540-42673-6). Lect. Notes Comput. Sci. 2211, 185-203 (2001). MSC: 68N18 × Cite Format Result Cite Review PDF Full Text: Link
Cáccamo, Mario; Winskel, Glynn A higher-order calculus for categories. (English) Zbl 1005.18001 Boulton, Richard J. (ed.) et al., Theorem proving in higher order logics. 14th international conference, TPHOLs 2001, Edinburgh, Scotland, GB, September 3-6, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2152, 136-153 (2001). MSC: 18A15 68T15 03B35 × Cite Format Result Cite Review PDF Full Text: Link
Zeilberger, Doron The umbral transfer-matrix method. I: Foundations. (English) Zbl 0961.05003 J. Comb. Theory, Ser. A 91, No. 1-2, 451-463 (2000). Reviewer: D.V.Chopra (Wichita) MSC: 05A40 05A15 × Cite Format Result Cite Review PDF Full Text: DOI
Galmiche, Didier; Pym, David J. Proof-search in type-theoretic languages: An introduction. (English) Zbl 0952.03006 Theor. Comput. Sci. 232, No. 1-2, 5-53 (2000). MSC: 03B35 03B15 03F03 68N18 03B70 × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF
Zeilberger, Doron Automated counting of Lego towers. (English) Zbl 0931.05022 J. Difference Equ. Appl. 5, No. 4-5, 323-333 (1999). Reviewer: H.N.V.Temperley (Langport) MSC: 05B50 05A15 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Kamareddine, Fairouz; Bloo, Roel; Nederpelt, Rob On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations. (English) Zbl 0930.03012 Ann. Pure Appl. Logic 97, No. 1-3, 27-45 (1999). MSC: 03B40 × Cite Format Result Cite Review PDF Full Text: DOI
Damiani, Ferruccio; Prost, Frédéric Detecting and removing dead-code using rank 2 intersection. (English) Zbl 0927.03050 Giménez, Eduardo (ed.) et al., Types for proofs and programs. International workshop TYPES ’96, Aussois, France, December 15–19, 1996. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1512, 66-87 (1998). MSC: 03B70 68N18 × Cite Format Result Cite Review PDF
Barthe, Gilles; Hatcliff, John; Thiemann, Peter Monadic type systems: Pure type systems for impure settings. (Preliminary report). (English) Zbl 0925.68294 Gordon, Andrew (ed.) et al., HOOTS II. 2nd workshop on higher-order operational techniques in semantics. Stanford Univ., Palo Alto, CA, USA, December 8–12, 1997. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 10, electronic paper No. 9 (1997). MSC: 68Q55 × Cite Format Result Cite Review PDF Full Text: Link
Parent-Vigouroux, Catherine Verifying programs in the calculus of inductive constructions. (English) Zbl 0905.68092 Formal Asp. Comput. 9, No. 5-6, 484-517 (1997). MSC: 68Q60 × Cite Format Result Cite Review PDF Full Text: DOI
Zenger, Christoph Indexed types. (English) Zbl 0893.68086 Theor. Comput. Sci. 187, No. 1-2, 147-165 (1997). MSC: 68W30 × Cite Format Result Cite Review PDF Full Text: DOI
Reus, Bernhard Synthetic domain theory in type theory: another logic of computable functions. (English) Zbl 07876672 von Wright, J. (ed.) et al., Theorem proving in higher order logics. 9th international conference, TPHOL ’96, Turku, Finland, August 26–30, 1996. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1125, 363-380 (1996). MSC: 68Q55 03B35 68N18 68Q60 68V15 × Cite Format Result Cite Review PDF Full Text: DOI
Gordon, Mike Set theory, higher order logic or both? (English) Zbl 07876661 von Wright, J. (ed.) et al., Theorem proving in higher order logics. 9th international conference, TPHOL ’96, Turku, Finland, August 26–30, 1996. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1125, 191-201 (1996). MSC: 68V15 03B16 03B35 03E99 × Cite Format Result Cite Review PDF Full Text: DOI
Mendler, Michael A timing refinement of intuitionistic proofs and its application to the timing analysis of combinational circuits. (English) Zbl 1412.68139 Migliolo, P. (ed.) et al., Theorem proving with analytic tableaux and related methods. 5th international workshop, TABLEAUX ’96, Terrasini, Palermo, Italy, May 15–17, 1996. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 1071, 261-277 (1996). MSC: 68Q60 03B20 03B70 68T15 94C10 × Cite Format Result Cite Review PDF Full Text: DOI
Pollack, Robert On extensibility of proof checkers. (English) Zbl 1530.68270 Dybjer, Peter (ed.) et al., Types for proofs and programs. International workshop TYPES ’94, Båstad, Sweden, June 6–10, 1994. Selected papers. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 996, 140-161 (1995). MSC: 68V15 × Cite Format Result Cite Review PDF Full Text: DOI
Reus, Bernhard Program verification in synthetic domain theory. (English) Zbl 0869.68037 München: Univ. München, Fak. f. Math. xii, 293 p. (1995). MSC: 68N99 68-02 03B15 × Cite Format Result Cite Review PDF
Miculan, Marino The expressive power of structural operational semantics with explicit assumptions. (English) Zbl 1527.68123 Barendregt, Henk (ed.) et al., TYPES ’93. Types for proofs and programs. International workshop, Nijmegen, the Netherlands, May 24–28, 1993. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 806, 263-290 (1994). MSC: 68Q55 68N15 68N18 × Cite Format Result Cite Review PDF Full Text: DOI Link
Magnusson, Lena; Nordström, Bengt The ALF proof editor and its proof engine. (English) Zbl 1527.68259 Barendregt, Henk (ed.) et al., TYPES ’93. Types for proofs and programs. International workshop, Nijmegen, the Netherlands, May 24–28, 1993. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 806, 213-237 (1994). MSC: 68V15 × Cite Format Result Cite Review PDF Full Text: DOI
Hofmann, Martin Elimination of extensionality in Martin-Löf type theory. (English) Zbl 1527.03009 Barendregt, Henk (ed.) et al., TYPES ’93. Types for proofs and programs. International workshop, Nijmegen, the Netherlands, May 24–28, 1993. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 806, 166-190 (1994). MSC: 03B38 03B70 × Cite Format Result Cite Review PDF Full Text: DOI
Jackson, Paul Exploring abstract algebra in constructive type theory. (English) Zbl 1433.68553 Bundy, Alan (ed.), Automated deduction – CADE-12. 12th international conference, Nancy, France, June 26 – July 1, 1994. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 814, 590-604 (1994). MSC: 68V15 20M05 68V20 × Cite Format Result Cite Review PDF Full Text: DOI
Dybjer, Peter Inductive families. (English) Zbl 0808.03044 Formal Asp. Comput. 6, No. 4, 440-465 (1994). MSC: 03F35 03B70 × Cite Format Result Cite Review PDF Full Text: DOI
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 × Cite Format Result Cite Review PDF
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 × Cite Format Result Cite Review PDF Full Text: DOI