×

Found 18 Documents (Results 1–18)

POSIX lexing with derivatives of regular expressions (proof pearl). (English) Zbl 1478.68118

Blanchette, Jasmin Christian (ed.) et al., Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9807, 69-86 (2016).
PDFBibTeX XMLCite
Full Text: DOI Link

A formal model and correctness proof for an access control policy framework. (English) Zbl 1426.68032

Gonthier, Georges (ed.) et al., Certified programs and proofs. Third international conference, CPP 2013, Melbourne, VIC, Australia, December 11–13, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8307, 292-307 (2013).
MSC:  68M25 68V15
PDFBibTeX XMLCite
Full Text: DOI

Mechanising Turing machines and computability theory in Isabelle/HOL. (English) Zbl 1317.68237

Blazy, Sandrine (ed.) et al., Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39633-5/pbk). Lecture Notes in Computer Science 7998, 147-162 (2013).
MSC:  68T15 68Q05
PDFBibTeX XMLCite
Full Text: DOI

Priority inheritance protocol proved correct. (English) Zbl 1360.68772

Beringer, Lennart (ed.) et al., Interactive theorem proving. Third international conference, ITP 2012, Princeton, NJ, USA, August 13–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32346-1/pbk). Lecture Notes in Computer Science 7406, 217-232 (2012).
MSC:  68T15 68M12
PDFBibTeX XMLCite
Full Text: DOI Link

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

General bindings and alpha-equivalence in Nominal Isabelle. (English) Zbl 1326.68265

Barthe, Gilles (ed.), Programming languages and systems. 20th European symposium on programming, ESOP 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-19717-8/pbk). Lecture Notes in Computer Science 6602, 480-500 (2011).
MSC:  68T15 68N15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Formal SOS-proofs for the \(\lambda\)-calculus. (English) Zbl 1310.68184

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, 139-155 (2009).
MSC:  68T15 03B40 68Q55 68Q60
PDFBibTeX XMLCite
Full Text: DOI

Nominal verification of algorithm \(W\). (English) Zbl 1195.68118

Bertot, Yves (ed.) et al., From semantics to computer science. Essays in honour of Gilles Kahn. Cambridge: Cambridge University Press (ISBN 978-0-521-51825-3/hbk). 363-382 (2009).
MSC:  68W40 68N17 68N18 68T15 68W05
PDFBibTeX XMLCite

Formalising in nominal Isabelle Crary’s completeness proof for equivalence checking. (English) Zbl 1278.68276

Pientka, B. (ed.) et al., Proceedings of the second international workshop on logical frameworks and meta-languages: theory and practice (LFMTP 2007), Bremen, Germany, July 15, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 196, 3-18 (2008).
MSC:  68T15 03B35 03B70
PDFBibTeX XMLCite
Full Text: Link

Revisiting cut-elimination: One difficult proof is really a proof. (English) Zbl 1146.68041

Voronkov, Andrei (ed.), Rewriting techniques and applications. 19th international conference, RTA 2008, Hagenberg, Austria, July 15–17, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-70588-8/pbk). Lecture Notes in Computer Science 5117, 409-424 (2008).
MSC:  68Q42 03F05 03B35 68T15
PDFBibTeX XMLCite
Full Text: DOI

A head-to-head comparison of de Bruijn indices and names. (English) Zbl 1278.03033

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, 53-67 (2007).
MSC:  03B40 03B70 68T15
PDFBibTeX XMLCite
Full Text: Link

A recursion combinator for nominal datatypes implemented in Isabelle/HOL. (English) Zbl 1222.68374

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, 498-512 (2006).
MSC:  68T15 68N18
PDFBibTeX XMLCite
Full Text: DOI

Nominal techniques in Isabelle/HOL. (English) Zbl 1135.68561

Nieuwenhuis, Robert (ed.), Automated deduction – CADE-20. 20th international conference on automated deduction, Tallinn, Estonia, July 22–27, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28005-7/pbk). Lecture Notes in Computer Science 3632. Lecture Notes in Artificial Intelligence, 38-53 (2005).
MSC:  68T15 03B35 03B40
PDFBibTeX XMLCite
Full Text: DOI

Filter Results by …

Document Type

all top 5

Year of Publication

Main Field

all top 3

Software