×

Found 164 Documents (Results 1–100)

A dependent dependency calculus. (English) Zbl 1528.68078

Sergey, Ilya (ed.), Programming languages and systems. 31st European symposium on programming, ESOP 2022, held as part of the European joint conferences on theory and practice of software, ETAPS 2022, Munich, Germany, April 2–7, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13240, 403-430 (2022).
MSC:  68N30 03B70 68N18
PDFBibTeX XMLCite
Full Text: DOI arXiv

\(\eta\)-equivalence in core dependent Haskell. (English) Zbl 07756112

Bezem, Marc (ed.) et al., 25th international conference on types for proofs and programs. TYPES 2019, June 11–14, 2019, Oslo, Norway. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 175, Article 7, 31 p. (2020).
MSC:  68N18
PDFBibTeX XMLCite
Full Text: DOI

A formalization of properties of continuous functions on closed intervals. (English) Zbl 1503.68298

Bigatti, Anna Maria (ed.) et al., Mathematical software – ICMS 2020. 7th international conference, Braunschweig, Germany, July 13–16, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12097, 272-280 (2020).
PDFBibTeX XMLCite
Full Text: DOI

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
PDFBibTeX XMLCite
Full Text: DOI

Reasoning about modular datatypes with Mendler induction. (English) Zbl 1476.68056

Matthes, Ralph (ed.) et al., Proceedings of the tenth international workshop on fixed points in computer science, FICS 2015, Berlin, Germany, September 11–12, 2015. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 191, 143-157 (2015).
MSC:  68N18 68Q55
PDFBibTeX XMLCite
Full Text: arXiv Link

Automath type inclusion in Barendregt’s cube. (English) Zbl 1466.68078

Beklemishev, Lev D. (ed.) et al., Computer science – theory and applications. 10th international computer science symposium in Russia, CSR 2015, Listvyanka, Russia, July 13–17, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9139, 262-282 (2015).
PDFBibTeX XMLCite
Full Text: DOI

Scalar System F for linear-algebraic \(\lambda\)-calculus: towards a quantum physical logic. (English) Zbl 1347.03019

Coecke, Bob (ed.) et al., Proceedings of the 6th international workshop on quantum physics and logic (QPL 2009), Oxford, UK, April 8–9, 2009. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 270, No. 2, 219-229 (2011).
MSC:  03B40 81P10
PDFBibTeX XMLCite
Full Text: DOI

A flexible framework for visualisation of computational properties of general explicit substitutions calculi. (English) Zbl 1347.68058

Haeusler, Edward Hermann (ed.) et al., Proceedings of the 5th workshop on logical and semantic frameworks, with applications (LSFA 2010), Natal, Brazil, August 31, 2010. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 269, 41-54 (2011).
MSC:  68N18 68Q42
PDFBibTeX XMLCite
Full Text: DOI

Refinement types as higher-order dependency pairs. (English) Zbl 1236.68147

Schmid-Schauß, Manfred (ed.), 22nd international conference on rewriting techniques and applications (RTA 2011), Novi Sad, Serbia, May 30 – June 1, 2011. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-30-9). LIPIcs – Leibniz International Proceedings in Informatics 10, 299-312, electronic only (2011).
MSC:  68Q42 68N30 68N18
PDFBibTeX XMLCite
Full Text: DOI Link

Realizability and parametricity in pure type systems. (English) Zbl 1326.68068

Hofmann, Martin (ed.), Foundations of software science and computational structures. 14th international conference, FOSSACS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19804-5/pbk). Lecture Notes in Computer Science 6604, 108-122 (2011).
MSC:  68N18 03B70 68N15
PDFBibTeX XMLCite
Full Text: DOI

Justification logic and history based computation. (English) Zbl 1286.03045

Cavalcanti, Ana (ed.) et al., Theoretical aspects of computing – ICTAC 2010. 7th international colloquium, Natal, Rio Grande do Norte, Brazil, September 1–3, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14807-1/pbk). Lecture Notes in Computer Science 6255, 337-351 (2010).
MSC:  03B42 03B40 68N18
PDFBibTeX XMLCite
Full Text: DOI

Introduction to type theory. (English) Zbl 1250.68088

Bove, Ana (ed.) et al., Language engineering and rigorous software development. International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24–March 1, 2008. Revised tutorial lectures. Berlin: Springer (ISBN 978-3-642-03152-6/pbk). Lecture Notes in Computer Science 5520, 1-56 (2009).
MSC:  68N18 03B40 68T15
PDFBibTeX XMLCite
Full Text: DOI Link

Inductive and coinductive components of corecursive functions in Coq. (English) Zbl 1279.68285

Adámek, J. (ed.) et al., Proceedings of the ninth workshop on coalgebraic methods in computer science (CMCS 2008), Budapest, Hungary, April 4–6, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 203, No. 5, 25-47 (2008).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI

Erasure and polymorphism in pure type systems. (English) Zbl 1138.68361

Amadio, Roberto (ed.), Foundations of software science and computational structures. 11th international conference, FOSSACS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29–April 6, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-78497-5/pbk). Lecture Notes in Computer Science 4962, 350-364 (2008).
MSC:  68N30 68N18
PDFBibTeX XMLCite
Full Text: DOI

Encoding functional relations in Scunak. (English) Zbl 1278.68250

Momigliano, Alberto (ed.) et al., Proceedings of the first international workshop on logical frameworks and meta-languages: theory and practice (LFMTP 2006), Seattle, WA, USA, August 16, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 174, No. 5, 127-139 (2007).
MSC:  68T15 03B70 03E99
PDFBibTeX XMLCite
Full Text: Link

Embedding pure type systems in the lambda-pi-calculus modulo. (English) Zbl 1215.03021

Ronchi della Rocca, Simona (ed.), Typed lambda calculi and applications. 8th international conference, TLCA 2007, Paris, France, June 26–28, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73227-3/pbk). Lecture Notes in Computer Science 4583, 102-117 (2007).
MSC:  03B40 03B70 68N18
PDFBibTeX XMLCite
Full Text: DOI arXiv HAL

Using first-order theorem provers in the Jahob data structure verification system. (English) Zbl 1132.68348

Cook, Byron (ed.) et al., Verification, model checking, and abstract interpretation. 8th international conference, VMCAI 2007, Nice, France, January 14–16, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-69735-0/pbk). Lecture Notes in Computer Science 4349, 74-88 (2007).
MSC:  68P05 68Q60 68T15
PDFBibTeX XMLCite
Full Text: DOI Link

Formal global optimisation with Taylor models. (English) Zbl 1222.68377

Furbach, Ulrich (ed.) et al., Automated reasoning. Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17–20, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-37187-8/pbk). Lecture Notes in Computer Science 4130. Lecture Notes in Artificial Intelligence, 408-422 (2006).
MSC:  68T15 90C26
PDFBibTeX XMLCite
Full Text: DOI Link

On the role of type decorations in the calculus of inductive constructions. (English) Zbl 1136.03305

Ong, Luke (ed.), Computer science logic. 19th international workshop, CSL 2005, 14th annual conference of the EACSL, Oxford, UK, August 22–25, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28231-9/pbk). Lecture Notes in Computer Science 3634, 151-166 (2005).
MSC:  03B35 68T15
PDFBibTeX XMLCite
Full Text: DOI

Decidability of type-checking in the calculus of algebraic constructions with size annotations. (English) Zbl 1136.68410

Ong, Luke (ed.), Computer science logic. 19th international workshop, CSL 2005, 14th annual conference of the EACSL, Oxford, UK, August 22–25, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28231-9/pbk). Lecture Notes in Computer Science 3634, 135-150 (2005).
PDFBibTeX XMLCite
Full Text: DOI

ATS: A language that combines programming with theorem proving. (English) Zbl 1171.68421

Gramlich, Bernhard (ed.), Frontiers of combining systems. 5th international workshop, FroCos 2005, Vienna, Austria, September 19–21, 2005. Proceedings. Berlin: Springer (ISBN 3-540-29051-6/pbk). Lecture Notes in Computer Science 3717. Lecture Notes in Artificial Intelligence, 310-320 (2005).
MSC:  68N30 68T15
PDFBibTeX XMLCite
Full Text: DOI

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
PDFBibTeX XMLCite
Full Text: DOI

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
PDFBibTeX XMLCite
Full Text: DOI

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).
MSC:  68T15 03B15 03B35 03B70 68N18 68Q60 68-01
PDFBibTeX XMLCite

Reducibility: a ubiquitous method in lambda calculus with intersection types. (English) Zbl 1270.03031

van Bakel, Steffen (ed.), ITRS’02. Proceedings of the 2nd workshop on intersection types and related systems (FLoC satellite event), Copenhagen, Denmark, July 26, 2002. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 70, No. 1, 106-123 (2003).
MSC:  03B40 68N18
PDFBibTeX XMLCite
Full Text: DOI

Strong normalization with singleton types. (English) Zbl 1270.03030

van Bakel, Steffen (ed.), ITRS’02. Proceedings of the 2nd workshop on intersection types and related systems (FLoC satellite event), Copenhagen, Denmark, July 26, 2002. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 70, No. 1, 53-71 (2003).
MSC:  03B40 68N18
PDFBibTeX XMLCite
Full Text: DOI

Tactics and parameters. (English) Zbl 1264.03042

Dahn, Ingo (ed.) et al., Proceedings of the workshop on mathematics, logic and computation (satellite event of ICALP 2003), Valencia, Spain, June 12–14, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 85, No. 7, 50-68 (2003).
MSC:  03B35 68T15
PDFBibTeX XMLCite
Full Text: DOI

First order logic with domain conditions. (English) Zbl 1279.68299

Basin, David (ed.) et al., Theorem proving in higher order logics. 16th international conference, TPHOLs 2003, Rome, Italy, September 8–12, 2003. Proceedings. Berlin: Springer (ISBN 3-540-40664-6/pbk). Lect. Notes Comput. Sci. 2758, 221-237 (2003).
MSC:  68T15 03B35
PDFBibTeX XMLCite
Full Text: DOI

Using theory morphisms for implementing formal methods tools. (English) Zbl 1023.68654

Geuvers, Herman (ed.) et al., Types for proofs and programs. International workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 2646, 59-77 (2003).
MSC:  68T15 68Q60 03B70
PDFBibTeX XMLCite
Full Text: Link

Filter Results by …

Document Type

all top 5

Author

all top 5

Year of Publication

all top 3

Main Field

all top 3

Software