×

Found 74 Documents (Results 1–74)

Newest Citations Relevance
Errington, Jacob; Jang, Junyoung; Pientka, Brigitte

Harpoon: mechanizing metatheory interactively. (English) Zbl 1540.68266

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 636-648 (2021).
MSC:  68V15
PDFBibTeX XMLCite
\textit{J. Errington} et al., Lect. Notes Comput. Sci. 12699, 636--648 (2021; Zbl 1540.68266)
Full Text: DOI
OA License
Georges, Aina Linn; Murawska, Agata; Otis, Shawn; Pientka, Brigitte

Lincx: a linear logical framework with first-class contexts. (English) Zbl 1485.68065

Yang, Hongseok (ed.), Programming languages and systems. 26th European symposium on programming, ESOP 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 10201, 530-555 (2017).
MSC:  68N30 03F52
PDFBibTeX XMLCite
\textit{A. L. Georges} et al., Lect. Notes Comput. Sci. 10201, 530--555 (2017; Zbl 1485.68065)
Full Text: DOI
Ferreira, Francisco; Pientka, Brigitte

Programs using syntax with first-class binders. (English) Zbl 1485.68064

Yang, Hongseok (ed.), Programming languages and systems. 26th European symposium on programming, ESOP 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 10201, 504-529 (2017).
MSC:  68N30 68N15 68N18
PDFBibTeX XMLCite
\textit{F. Ferreira} and \textit{B. Pientka}, Lect. Notes Comput. Sci. 10201, 504--529 (2017; Zbl 1485.68064)
Full Text: DOI
Crole, Roy L.; Furniss, Amy

Canonical HybridLF: extending Hybrid with dependent types. (English) Zbl 1394.68351

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, 125-142 (2016).
MSC:  68T15 03B35 03B40
PDFBibTeX XMLCite
\textit{R. L. Crole} and \textit{A. Furniss}, Electron. Notes Theor. Comput. Sci. 323, 125--142 (2016; Zbl 1394.68351)
Full Text: DOI
Libal, Tomer; Miller, Dale

Functions-as-constructors higher-order unification. (English) Zbl 1387.03008

Kesner, Delia (ed.) et al., 1st international conference on formal structures for computation and deduction, FSCD 2016, Porto, Portugal, June 22–26, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-010-1). LIPIcs – Leibniz International Proceedings in Informatics 52, Article 26, 17 p. (2016).
MSC:  03B35 68Q42 68T15
PDFBibTeX XMLCite
\textit{T. Libal} and \textit{D. Miller}, LIPIcs -- Leibniz Int. Proc. Inform. 52, Article 26, 17 p. (2016; Zbl 1387.03008)
Full Text: DOI
Oliveira, Bruno C. d. S.; Shi, Zhiyuan; Alpuim, João

Disjoint intersection types. (English) Zbl 1361.68046

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). 364-377 (2016).
MSC:  68N18
PDFBibTeX XMLCite
\textit{B. C. d. S. Oliveira} 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). 364--377 (2016; Zbl 1361.68046)
Full Text: DOI
Feltman, Nicolas; Angiuli, Carlo; Acar, Umut A.; Fatahalian, Kayvon

Automatically splitting a two-stage lambda calculus. (English) Zbl 1335.68032

Thiemann, Peter (ed.), Programming languages and systems. 25th European symposium on programming, ESOP 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer (ISBN 978-3-662-49497-4/pbk; 978-3-662-49498-1/ebook). Lecture Notes in Computer Science 9632, 255-281 (2016).
MSC:  68N18 68T15
PDFBibTeX XMLCite
\textit{N. Feltman} et al., Lect. Notes Comput. Sci. 9632, 255--281 (2016; Zbl 1335.68032)
Full Text: DOI
Eisenberg, Richard A.; Weirich, Stephanie; Ahmed, Hamidhasan G.

Visible type application. (English) Zbl 1335.68031

Thiemann, Peter (ed.), Programming languages and systems. 25th European symposium on programming, ESOP 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer (ISBN 978-3-662-49497-4/pbk; 978-3-662-49498-1/ebook). Lecture Notes in Computer Science 9632, 229-254 (2016).
MSC:  68N18
PDFBibTeX XMLCite
\textit{R. A. Eisenberg} et al., Lect. Notes Comput. Sci. 9632, 229--254 (2016; Zbl 1335.68031)
Full Text: DOI Link
Miller, Dale

Proof checking and logic programming. (English) Zbl 1362.68055

Falaschi, Moreno (ed.), Logic-based program synthesis and transformation. 25th international symposium, LOPSTR 2015, Siena, Italy, July 13–15, 2015. Revised selected papers. Cham: Springer (ISBN 978-3-319-27435-5/pbk; 978-3-319-27436-2/ebook). Lecture Notes in Computer Science 9527, 3-17 (2015).
MSC:  68N30 03B70 68N17
PDFBibTeX XMLCite
\textit{D. Miller}, Lect. Notes Comput. Sci. 9527, 3--17 (2015; Zbl 1362.68055)
Full Text: DOI HAL
Rabe, Florian

Generic literals. (English) Zbl 1417.68216

Kerber, Manfred (ed.) et al., Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9150, 102-117 (2015).
MSC:  68T30
PDFBibTeX XMLCite
\textit{F. Rabe}, Lect. Notes Comput. Sci. 9150, 102--117 (2015; Zbl 1417.68216)
Full Text: DOI
Horozal, Fulya; Rabe, Florian; Kohlhase, Michael

Flexary operators for formalized mathematics. (English) Zbl 1304.68171

Watt, Stephen M. (ed.) et al., Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-08433-6/pbk). Lecture Notes in Computer Science 8543. Lecture Notes in Artificial Intelligence, 312-327 (2014).
MSC:  68T30
PDFBibTeX XMLCite
\textit{F. Horozal} et al., Lect. Notes Comput. Sci. 8543, 312--327 (2014; Zbl 1304.68171)
Full Text: DOI
Dunfield, Joshua

Elaborating intersection and union types. (English) Zbl 1291.68140

Proceedings of the 17th ACM SIGPLAN international conference on functional programming, ICFP ’12, Copenhagen, Denmark, September 9–15, 2012. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-1054-3). ACM SIGPLAN Notices 47, No. 9, 17-28 (2012).
MSC:  68N30 68N18
PDFBibTeX XMLCite
\textit{J. Dunfield}, in: Proceedings of the 17th ACM SIGPLAN international conference on functional programming, ICFP '12, Copenhagen, Denmark, September 9--15, 2012. New York, NY: Association for Computing Machinery (ACM). 17--28 (2012; Zbl 1291.68140)
Full Text: DOI arXiv
Accattoli, Beniamino

Proof pearl: Abella formalization of \(\lambda \)-calculus cube property. (English) Zbl 1385.68012

Hawblitzel, Chris (ed.) et al., Certified programs and proofs. Second international conference, CPP 2012, Kyoto, Japan, December 13–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-35307-9/pbk). Lecture Notes in Computer Science 7679, 173-187 (2012).
MSC:  68N18 68T15
PDFBibTeX XMLCite
\textit{B. Accattoli}, Lect. Notes Comput. Sci. 7679, 173--187 (2012; Zbl 1385.68012)
Full Text: DOI
Tollitte, Pierre-Nicolas; Delahaye, David; Dubois, Catherine

Producing certified functional code from inductive specifications. (English) Zbl 1383.68018

Hawblitzel, Chris (ed.) et al., Certified programs and proofs. Second international conference, CPP 2012, Kyoto, Japan, December 13–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-35307-9/pbk). Lecture Notes in Computer Science 7679, 76-91 (2012).
MSC:  68N18 68T15
PDFBibTeX XMLCite
\textit{P.-N. Tollitte} et al., Lect. Notes Comput. Sci. 7679, 76--91 (2012; Zbl 1383.68018)
Full Text: DOI
Licata, Daniel R.; Harper, Robert

2-dimensional directed type theory. (English) Zbl 1343.03051

Mislove, Michael (ed.) et al., Proceedings of the 27th conference on the mathematical foundations of programming semantics (MFPS XXVII), Pittsburgh, PA, USA, May 25–28, 2011. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 276, 263-289 (2011).
MSC:  03G30 03B15 18D05 55U40 68N30
PDFBibTeX XMLCite
\textit{D. R. Licata} and \textit{R. Harper}, Electron. Notes Theor. Comput. Sci. 276, 263--289 (2011; Zbl 1343.03051)
Full Text: DOI
Cheney, James; Urban, Christian

Mechanizing the metatheory of mini-XQuery. (English) Zbl 1350.68054

Jouannaud, Jean-Pierre (ed.) et al., Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7–9, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-25378-2/pbk). Lecture Notes in Computer Science 7086, 280-295 (2011).
MSC:  68N15 68N18 68T15
PDFBibTeX XMLCite
\textit{J. Cheney} and \textit{C. Urban}, Lect. Notes Comput. Sci. 7086, 280--295 (2011; Zbl 1350.68054)
Full Text: DOI
Abel, Andreas; Pientka, Brigitte

Higher-order dynamic pattern unification for dependent types and records. (English) Zbl 1331.68040

Ong, Luke (ed.), Typed lambda calculi and applications. 10th international conference, TLCA 2011, Novi Sad, Serbia, June 1–3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-21690-9/pbk; 978-3-642-21691-6/ebook). Lecture Notes in Computer Science 6690, 10-26 (2011).
MSC:  68N18
PDFBibTeX XMLCite
\textit{A. Abel} and \textit{B. Pientka}, Lect. Notes Comput. Sci. 6690, 10--26 (2011; Zbl 1331.68040)
Full Text: DOI
Pientka, Brigitte

Programming inductive proofs. A new approach based on contextual types. (English) Zbl 1309.68051

Siegler, Simon (ed.) et al., Verification, induction, termination analysis. Festschrift for Christoph Walther on the occasion of his 60th birthday. Berlin: Springer (ISBN 978-3-642-17171-0/pbk). Lecture Notes in Computer Science 6463. Lecture Notes in Artificial Intelligence, 1-16 (2010).
MSC:  68N30 68Q60
PDFBibTeX XMLCite
\textit{B. Pientka}, Lect. Notes Comput. Sci. 6463, 1--16 (2010; Zbl 1309.68051)
Full Text: DOI
Pientka, Brigitte; Dunfield, Joshua

Beluga: a framework for programming and reasoning with deductive systems (system description). (English) Zbl 1291.68366

Giesl, Jürgen (ed.) et al., Automated reasoning. 5th international joint conference, IJCAR 2010, Edinburgh, UK, July 16–19, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14202-4/pbk). Lecture Notes in Computer Science 6173. Lecture Notes in Artificial Intelligence, 15-21 (2010).
MSC:  68T15
PDFBibTeX XMLCite
\textit{B. Pientka} and \textit{J. Dunfield}, Lect. Notes Comput. Sci. 6173, 15--21 (2010; Zbl 1291.68366)
Full Text: DOI
Dunfield, Joshua; Pientka, Brigitte

Case analysis of higher-order data. (English) Zbl 1337.68058

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, 69-84 (2009).
MSC:  68N18 03B70 68T15
PDFBibTeX XMLCite
\textit{J. Dunfield} and \textit{B. Pientka}, Electron. Notes Theor. Comput. Sci. 228, 69--84 (2009; Zbl 1337.68058)
Full Text: DOI
Miller, Dale

Formalizing operational semantic specifications in logic. (English) Zbl 1347.68213

Falaschi, Moreno (ed.), Proceedings of the 17th international workshop on functional and (constraint) logic programming (WFLP 2008), Siena, Italy, July 3–4, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 246, 147-165 (2009).
MSC:  68Q55 03B70 68Q42 68Q60
PDFBibTeX XMLCite
\textit{D. Miller}, Electron. Notes Theor. Comput. Sci. 246, 147--165 (2009; Zbl 1347.68213)
Full Text: DOI
Reed, Jason; Pfenning, Frank

Intuitionistic letcc via labelled deduction. (English) Zbl 1347.03061

Areces, Carlos (ed.) et al., Proceedings of the 5th workshop on methods for modalities (M4M5 2007), Cachan, France, November 29–30, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 231, 91-111 (2009).
MSC:  03B70 03B20 03B40 03B45 68N18 68T15
PDFBibTeX XMLCite
\textit{J. Reed} and \textit{F. Pfenning}, Electron. Notes Theor. Comput. Sci. 231, 91--111 (2009; Zbl 1347.03061)
Full Text: DOI
Abel, Andreas; Coquand, Thierry; Dybjer, Peter

Verifying a semantic \(\beta \eta \)-conversion test for Martin-Löf type theory. (English) Zbl 1157.68025

Audebaud, Philippe (ed.) et al., Mathematics of program construction. 9th international conference, MPC 2008, Marseille, France, July 15–18, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-70593-2/pbk). Lecture Notes in Computer Science 5133, 29-56 (2008).
MSC:  68N30 68N18 68T15
PDFBibTeX XMLCite
\textit{A. Abel} et al., Lect. Notes Comput. Sci. 5133, 29--56 (2008; Zbl 1157.68025)
Full Text: DOI
Sewell, Peter; Nardelli, Francesco Zappa; Owens, Scott; Peskine, Gilles; Ridge, Thomas; Sarkar, Susmit; Strniša, Rok

Ott, effective tool support for the working semanticist. (English) Zbl 1291.68238

Proceedings of the 12th ACM SIGPLAN international conference on functional programming, ICFP ’07, Freiburg, Germany, October 1–3, 2007. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-59593-815-2). ACM SIGPLAN Notices 42, No. 9, 1-12 (2007).
MSC:  68Q55 68N15 68T15
PDFBibTeX XMLCite
\textit{P. Sewell} et al., in: Proceedings of the 12th ACM SIGPLAN international conference on functional programming, ICFP '07, Freiburg, Germany, October 1--3, 2007. New York, NY: Association for Computing Machinery (ACM). 1--12 (2007; Zbl 1291.68238)
Full Text: DOI
Brown, Chad E.

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
\textit{C. E. Brown}, Electron. Notes Theor. Comput. Sci. 174, No. 5, 127--139 (2007; Zbl 1278.68250)
Full Text: Link
Sheard, Tim; Pasalic, Emir

Meta-programming with built-in type equality. (English) Zbl 1278.68062

Schürmann, C. (ed.), Proceedings of the fourth international workshop on logical frameworks and meta-languages (LFM 2004), Cork, UK, July 5, 2004. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 199, 49-65 (2008).
MSC:  68N18 68Q55
PDFBibTeX XMLCite
\textit{T. Sheard} and \textit{E. Pasalic}, Electron. Notes Theor. Comput. Sci. 199, 49--65 (2007; Zbl 1278.68062)
Full Text: DOI
Reed, Jason

Hybridizing a logical framework. (English) Zbl 1278.03049

Blackburn, Patrick (ed.) et al., Proceedings of the international workshop on hybrid logic (HyLo 2006), Seattle, WA, USA, August 11, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 174, No. 6, 135-148 (2007).
MSC:  03B45 03B47 03B70
PDFBibTeX XMLCite
\textit{J. Reed}, Electron. Notes Theor. Comput. Sci. 174, No. 6, 135--148 (2007; Zbl 1278.03049)
Full Text: DOI
Pientka, Brigitte

Functional programming with higher-order abstract syntax and explicit substitutions. (English) Zbl 1277.68050

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, 41-60 (2007).
MSC:  68N18 68N30
PDFBibTeX XMLCite
\textit{B. Pientka}, Electron. Notes Theor. Comput. Sci. 174, No. 7, 41--60 (2007; Zbl 1277.68050)
Full Text: DOI
Rabe, Florian

First-order logic with dependent types. (English) Zbl 1222.03016

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, 377-391 (2006).
MSC:  03B35 03B10 03B15 03C07 68T15
PDFBibTeX XMLCite
\textit{F. Rabe}, Lect. Notes Comput. Sci. 4130, 377--391 (2006; Zbl 1222.03016)
Full Text: DOI
McLaughlin, Sean

An interpretation of Isabelle/HOL in HOL Light. (English) Zbl 1222.68370

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, 192-204 (2006).
MSC:  68T15 03B15
PDFBibTeX XMLCite
\textit{S. McLaughlin}, Lect. Notes Comput. Sci. 4130, 192--204 (2006; Zbl 1222.68370)
Full Text: DOI
Dijkstra, Atze; Swierstra, S. Doaitse

Ruler: Programming type rules. (English) Zbl 1185.68191

Hagiya, Masami (ed.) et al., Functional and logic programming. 8th international symposium, FLOPS 2006, Fuji-Susono, Japan, April 24–26, 2006. Proceedings. Berlin: Springer (ISBN 3-540-33438-6/pbk). Lecture Notes in Computer Science 3945, 30-46 (2006).
MSC:  68N18
PDFBibTeX XMLCite
\textit{A. Dijkstra} and \textit{S. D. Swierstra}, Lect. Notes Comput. Sci. 3945, 30--46 (2006; Zbl 1185.68191)
Full Text: DOI Link
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
PDFBibTeX XMLCite
\textit{E. Westbrook} et al., in: 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). 268--279 (2005; Zbl 1302.68095)
Full Text: DOI Link
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
PDFBibTeX XMLCite
\textit{C. Schürmann}, Lect. Notes Comput. Sci. 2998, 22--23 (2004; Zbl 1122.68391)
Full Text: DOI
Anderson, Penny; Pfenning, Frank

Verifying uniqueness in a logical framework. (English) Zbl 1099.68720

Slind, Konrad (ed.) et al., Theorem proving in higher order logics. 17th international conference, TPHOLs 2004, Park City, Utah, USA, September 14–17, 2004. Proceedings. Berlin: Springer (ISBN 3-540-23017-3/pbk). Lecture Notes in Computer Science 3223, 18-33 (2004).
MSC:  68T15 03B35 03B40
PDFBibTeX XMLCite
\textit{P. Anderson} and \textit{F. Pfenning}, Lect. Notes Comput. Sci. 3223, 18--33 (2004; Zbl 1099.68720)
Full Text: DOI
Hamid, Nadeem Abdul; Shao, Zhong

Interfacing Hoare logic and type systems for foundational proof-carrying code. (English) Zbl 1099.68726

Slind, Konrad (ed.) et al., Theorem proving in higher order logics. 17th international conference, TPHOLs 2004, Park City, Utah, USA, September 14–17, 2004. Proceedings. Berlin: Springer (ISBN 3-540-23017-3/pbk). Lecture Notes in Computer Science 3223, 118-135 (2004).
MSC:  68T15 03B35
PDFBibTeX XMLCite
\textit{N. A. Hamid} and \textit{Z. Shao}, Lect. Notes Comput. Sci. 3223, 118--135 (2004; Zbl 1099.68726)
Full Text: DOI
Schürmann, Carsten; Pfenning, Frank

A coverage checking algorithm for LF. (English) Zbl 1279.68295

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, 120-135 (2003).
MSC:  68T15 03B35 68N18
PDFBibTeX XMLCite
\textit{C. Schürmann} and \textit{F. Pfenning}, Lect. Notes Comput. Sci. 2758, 120--135 (2003; Zbl 1279.68295)
Full Text: DOI Link
Momigliano, Alberto; Ambler, Simon J.; Crole, Roy L.

A hybrid encoding of Howe’s method for establishing congruence of bisimilarity. (English) Zbl 1270.68072

Pfenning, Frank (ed.), LFM 2002. Proceedings of the 3rd international workshop on logical frameworks and meta-languages (FLoC satellite event), Copenhagen, Denmark, July 26, 2002. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 70, No. 2, 60-75 (2002).
MSC:  68N18 68T15
PDFBibTeX XMLCite
\textit{A. Momigliano} et al., Electron. Notes Theor. Comput. Sci. 70, No. 2, 60--75 (2002; Zbl 1270.68072)
Full Text: Link
Abel, Andreas

A third-order representation of the \(\lambda\mu\)-calculus. (English) Zbl 1268.68045

Ambler, S. J. (ed.) et al., MERLIN 2001. Proceedings of the workshop on mechanized reasoning about languages with variable binding (in connection with IJCAR 2001), Siena, Italy, June 18, 2001. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 58, No. 1, 97-114 (2001).
MSC:  68N18 68N17
PDFBibTeX XMLCite
\textit{A. Abel}, Electron. Notes Theor. Comput. Sci. 58, No. 1, 97--114 (2001; Zbl 1268.68045)
Full Text: DOI
Schürmann, Carsten; Yu, Dachuan; Ni, Zhaozhong

A representation of \(F_{\omega}\) in LF. (English) Zbl 1268.68055

Ambler, S. J. (ed.) et al., MERLIN 2001. Proceedings of the workshop on mechanized reasoning about languages with variable binding (in connection with IJCAR 2001), Siena, Italy, June 18, 2001. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 58, No. 1, 79-96 (2001).
MSC:  68N18 68T15 68N30
PDFBibTeX XMLCite
\textit{C. Schürmann} et al., Electron. Notes Theor. Comput. Sci. 58, No. 1, 79--96 (2001; Zbl 1268.68055)
Full Text: DOI
Miculan, Marino

Developing (meta)theory of \(\lambda\)-calculus in the theory of contexts. (English) Zbl 1268.68050

Ambler, S. J. (ed.) et al., MERLIN 2001. Proceedings of the workshop on mechanized reasoning about languages with variable binding (in connection with IJCAR 2001), Siena, Italy, June 18, 2001. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 58, No. 1, 37-58 (2001).
MSC:  68N18 68T15
PDFBibTeX XMLCite
\textit{M. Miculan}, Electron. Notes Theor. Comput. Sci. 58, No. 1, 37--58 (2001; Zbl 1268.68050)
Full Text: DOI

Filter Results by …

Document Type

all top 5

Author

all top 5

Serial

all top 5

Year of Publication

all top 3

Main Field

all top 3

Software