Saito, Ayumu; Affeldt, Reynald Towards a practical library for monadic equational reasoning in Coq. (English) Zbl 07705361 Komendantskaya, Ekaterina (ed.), Mathematics of program construction. 14th international conference, MPC 2022, Tbilisi, Georgia, September 26–28, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13544, 151-177 (2022). MSC: 68N30 PDFBibTeX XMLCite \textit{A. Saito} and \textit{R. Affeldt}, Lect. Notes Comput. Sci. 13544, 151--177 (2022; Zbl 07705361) Full Text: DOI
Larchey-Wendling, Dominique; Monin, Jean-François The Braga method: extracting certified algorithms from complex recursive schemes in Coq. (English) Zbl 1528.68392 Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 305-386 (2022). MSC: 68V15 68N19 68N30 PDFBibTeX XMLCite \textit{D. Larchey-Wendling} and \textit{J.-F. Monin}, in: Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school ``Proof and computation'', September 20--26, 2019. Hackensack, NJ: World Scientific. 305--386 (2022; Zbl 1528.68392) Full Text: DOI HAL
Farzan, Azadeh; Nicolet, Victor Counterexample-guided partial bounding for recursive function synthesis. (English) Zbl 1493.68107 Silva, Alexandra (ed.) et al., Computer aided verification. 33rd international conference, CAV 2021, virtual event, July 20–23, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12759, 832-855 (2021). MSC: 68N30 68N18 PDFBibTeX XMLCite \textit{A. Farzan} and \textit{V. Nicolet}, Lect. Notes Comput. Sci. 12759, 832--855 (2021; Zbl 1493.68107) Full Text: DOI
Di Stasio, Antonio; Murano, Aniello; Prignano, Vincenzo; Sorrentino, Loredana Improving parity games in practice. (English) Zbl 1507.68184 Ann. Math. Artif. Intell. 89, No. 5-6, 551-574 (2021). MSC: 68Q60 91A43 91A80 PDFBibTeX XMLCite \textit{A. Di Stasio} et al., Ann. Math. Artif. Intell. 89, No. 5--6, 551--574 (2021; Zbl 1507.68184) Full Text: DOI
Charguéraud, Arthur; Pottier, François Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. (English) Zbl 1468.68120 J. Autom. Reasoning 62, No. 3, 331-365 (2019). MSC: 68Q60 03B70 68N18 68P05 68V20 PDFBibTeX XMLCite \textit{A. Charguéraud} and \textit{F. Pottier}, J. Autom. Reasoning 62, No. 3, 331--365 (2019; Zbl 1468.68120) Full Text: DOI HAL
Moore, Brandon; Peña, Lucas; Rosu, Grigore Program verification by coinduction. (English) Zbl 1418.68060 Ahmed, Amal (ed.), Programming languages and systems. 27th European symposium on programming, ESOP 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10801, 589-618 (2018). MSC: 68N30 68Q55 68Q60 68T15 PDFBibTeX XMLCite \textit{B. Moore} et al., Lect. Notes Comput. Sci. 10801, 589--618 (2018; Zbl 1418.68060) Full Text: DOI
Saleh, Amr Hany; Karachalias, Georgios; Pretnar, Matija; Schrijvers, Tom Explicit effect subtyping. (English) Zbl 1418.68065 Ahmed, Amal (ed.), Programming languages and systems. 27th European symposium on programming, ESOP 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10801, 327-354 (2018). MSC: 68N30 68N15 68N18 PDFBibTeX XMLCite \textit{A. H. Saleh} et al., Lect. Notes Comput. Sci. 10801, 327--354 (2018; Zbl 1418.68065) Full Text: DOI arXiv
Hoffmann, Jan; Das, Ankush; Weng, Shu-Chun Towards automatic resource bound analysis for OCaml. (English) Zbl 1380.68123 Castagna, Giuseppe (ed.) et al., Proceedings of the 44th annual ACM SIGPLAN symposium on principles of programming languages, POPL ’17, Paris, France, January 15–21, 2017. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4660-3). 359-373 (2017). MSC: 68N30 68N15 68N20 PDFBibTeX XMLCite \textit{J. Hoffmann} et al., in: Proceedings of the 44th annual ACM SIGPLAN symposium on principles of programming languages, POPL '17, Paris, France, January 15--21, 2017. New York, NY: Association for Computing Machinery (ACM). 359--373 (2017; Zbl 1380.68123) Full Text: DOI arXiv
Padovani, Luca Context-free session type inference. (English) Zbl 1485.68072 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, 804-830 (2017). MSC: 68N30 68N15 68N18 68Q85 PDFBibTeX XMLCite \textit{L. Padovani}, Lect. Notes Comput. Sci. 10201, 804--830 (2017; Zbl 1485.68072) Full Text: DOI HAL
Guéneau, Armaël; Myreen, Magnus O.; Kumar, Ramana; Norrish, Michael Verified characteristic formulae for CakeML. (English) Zbl 1485.68030 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, 584-610 (2017). MSC: 68N15 68N18 68N30 PDFBibTeX XMLCite \textit{A. Guéneau} et al., Lect. Notes Comput. Sci. 10201, 584--610 (2017; Zbl 1485.68030) 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
Castagna, Giuseppe; Petrucciani, Tommaso; Nguyen, Kim Set-theoretic types for polymorphic variants. (English) Zbl 1360.68318 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). 387-391 (2016). MSC: 68N18 68N30 PDFBibTeX XMLCite \textit{G. Castagna} 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). 387--391 (2016; Zbl 1360.68318) Full Text: DOI arXiv HAL
Dagand, Pierre-Evariste; Tabareau, Nicolas; Tanter, Éric Partial type equivalences for verified dependent interoperability. (English) Zbl 1360.68322 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). 298-310 (2016). MSC: 68N18 68Q60 68T15 PDFBibTeX XMLCite \textit{P.-E. Dagand} 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). 298--310 (2016; Zbl 1360.68322) Full Text: DOI HAL
Lesani, Mohsen; Bell, Christian J.; Chlipala, Adam Chapar: certified causally consistent distributed key-value stores. (English) Zbl 1347.68117 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). 357-370 (2016). MSC: 68P20 68Q55 68Q60 68T15 PDFBibTeX XMLCite \textit{M. Lesani} et al., 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). 357--370 (2016; Zbl 1347.68117) Full Text: DOI
Yallop, Jeremy; Sheets, David; Madhavapeddy, Anil Declarative foreign function binding through generic programming. (English) Zbl 1475.68098 Kiselyov, Oleg (ed.) et al., Functional and logic programming. 13th international symposium, FLOPS 2016, Kochi, Japan, March 4–6, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9613, 198-214 (2016). MSC: 68N30 PDFBibTeX XMLCite \textit{J. Yallop} et al., Lect. Notes Comput. Sci. 9613, 198--214 (2016; Zbl 1475.68098) Full Text: DOI
Maréchal, Alexandre; Fouilhé, Alexis; King, Tim; Monniaux, David; Périn, Michael Polyhedral approximation of multivariate polynomials using Handelman’s theorem. (English) Zbl 1475.68093 Jobstmann, Barbara (ed.) et al., Verification, model checking, and abstract interpretation. 17th international conference, VMCAI 2016, St. Petersburg, FL, USA, January 17–19, 2016. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9583, 166-184 (2016). MSC: 68N30 52B55 68T20 90C90 PDFBibTeX XMLCite \textit{A. Maréchal} et al., Lect. Notes Comput. Sci. 9583, 166--184 (2016; Zbl 1475.68093) Full Text: DOI HAL
Jeannin, Jean-Baptiste; Kozen, Dexter; Silva, Alexandra Well-founded coalgebras, revisited. (English) Zbl 1376.68094 Math. Struct. Comput. Sci. 27, No. 7, 1111-1131 (2017). MSC: 68Q65 68N30 PDFBibTeX XMLCite \textit{J.-B. Jeannin} et al., Math. Struct. Comput. Sci. 27, No. 7, 1111--1131 (2015; Zbl 1376.68094) Full Text: DOI
Danvy, Olivier; Keller, Chantal; Puech, Matthias Typeful normalization by evaluation. (English) Zbl 1367.68051 Herbelin, Hugo (ed.) et al., 20th international conference on types for proofs and programs, TYPES’14, Paris, France, May 12–15, 2014. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-88-0). LIPIcs – Leibniz International Proceedings in Informatics 39, 72-88 (2015). MSC: 68N18 68N30 68Q65 PDFBibTeX XMLCite \textit{O. Danvy} et al., LIPIcs -- Leibniz Int. Proc. Inform. 39, 72--88 (2015; Zbl 1367.68051) Full Text: DOI
Rossberg, Andreas 1ML – core and modules united (F-ing first-class modules). (English) Zbl 1360.68338 Proceedings of the 20th ACM SIGPLAN international conference on functional programming, ICFP ’15, Vancouver, Canada, September 1–3, 2015. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-3669-7). 35-47 (2015). MSC: 68N18 03B70 68N15 68N30 68Q65 PDFBibTeX XMLCite \textit{A. Rossberg}, in: Proceedings of the 20th ACM SIGPLAN international conference on functional programming, ICFP '15, Vancouver, Canada, September 1--3, 2015. New York, NY: Association for Computing Machinery (ACM). 35--47 (2015; Zbl 1360.68338) Full Text: DOI
Delaware, Benjamin; Pit-Claudel, Clément; Gross, Jason; Chlipala, Adam Fiat: deductive synthesis of abstract data types in a proof assistant. (English) Zbl 1346.68175 Proceedings of the 42nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’15, Mumbai, India, January 12–18, 2015. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-3300-9). 689-700 (2015). MSC: 68T15 68N18 68Q60 68Q65 PDFBibTeX XMLCite \textit{B. Delaware} et al., in: Proceedings of the 42nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '15, Mumbai, India, January 12--18, 2015. New York, NY: Association for Computing Machinery (ACM). 689--700 (2015; Zbl 1346.68175) Full Text: DOI
Tan, Gang JNI light: an operational model for the core JNI. (English) Zbl 1361.68068 Math. Struct. Comput. Sci. 25, No. 4, 805-840 (2015). MSC: 68N30 68N15 PDFBibTeX XMLCite \textit{G. Tan}, Math. Struct. Comput. Sci. 25, No. 4, 805--840 (2015; Zbl 1361.68068) Full Text: DOI
Montenegro, Manuel; Peña, Ricardo; Sánchez-Hernández, Jaime A generic intermediate representation for verification condition generation. (English) Zbl 1473.68051 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. Lect. Notes Comput. Sci. 9527, 227-243 (2015). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{M. Montenegro} et al., Lect. Notes Comput. Sci. 9527, 227--243 (2015; Zbl 1473.68051) Full Text: DOI
Charguéraud, Arthur; Pottier, François Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. (English) Zbl 1465.68172 Urban, Christian (ed.) et al., Interactive theorem proving. 6th international conference, ITP 2015, Nanjing, China, August 24–27, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9236, 137-153 (2015). MSC: 68Q60 03B70 68N19 68P05 68V20 PDFBibTeX XMLCite \textit{A. Charguéraud} and \textit{F. Pottier}, Lect. Notes Comput. Sci. 9236, 137--153 (2015; Zbl 1465.68172) Full Text: DOI HAL
Bauer, Andrej; Pretnar, Matija Programming with algebraic effects and handlers. (English) Zbl 1304.68025 J. Log. Algebr. Methods Program. 84, No. 1, 108-123 (2015). MSC: 68N15 68N30 PDFBibTeX XMLCite \textit{A. Bauer} and \textit{M. Pretnar}, J. Log. Algebr. Methods Program. 84, No. 1, 108--123 (2015; Zbl 1304.68025) Full Text: DOI arXiv
Mulligan, Dominic P.; Owens, Scott; Gray, Kathryn E.; Ridge, Tom; Sewell, Peter Lem: reusable engineering of real-world semantics. (English) Zbl 1346.68123 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). 175-188 (2014). MSC: 68Q60 68Q55 68T15 PDFBibTeX XMLCite \textit{D. P. Mulligan} et al., 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). 175--188 (2014; Zbl 1346.68123) Full Text: DOI
Li, Liyi; Gunter, Elsa; Mansky, William Symbolic analysis tools for CSP. (English) Zbl 1432.68311 Ciobanu, Gabriel (ed.) et al., Theoretical aspects of computing – ICTAC 2014. 11th international colloquium, Bucharest, Romania, September 17–19, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8687, 295-313 (2014). MSC: 68Q85 68Q60 68V15 PDFBibTeX XMLCite \textit{L. Li} et al., Lect. Notes Comput. Sci. 8687, 295--313 (2014; Zbl 1432.68311) Full Text: DOI
Gao, Jianhua; Jiang, Ying Coinduction-based solution for minimization of Kripke structures. (Chinese. English summary) Zbl 1313.68075 J. Softw. 25, No. 1, 16-26 (2014). MSC: 68Q60 03B70 68Q65 PDFBibTeX XMLCite \textit{J. Gao} and \textit{Y. Jiang}, J. Softw. 25, No. 1, 16--26 (2014; Zbl 1313.68075) Full Text: DOI
Kuwahara, Takuya; Terauchi, Tachio; Unno, Hiroshi; Kobayashi, Naoki Automatic termination verification for higher-order functional programs. (English) Zbl 1347.68231 Shao, Zhong (ed.), Programming languages and systems. 23rd European symposium on programming, ESOP 2014, held as part of the European joint conferences on theory and practice of software, ETAPS 2014, Grenoble, France, April 5–13, 2014. Proceedings. Berlin: Springer (ISBN 978-3-642-54832-1/pbk). Lecture Notes in Computer Science 8410, 392-411 (2014). MSC: 68Q60 68N18 PDFBibTeX XMLCite \textit{T. Kuwahara} et al., Lect. Notes Comput. Sci. 8410, 392--411 (2014; Zbl 1347.68231) Full Text: DOI
Zhang, Danfeng; Myers, Andrew C. Toward general diagnosis of static errors. (English) Zbl 1284.68141 Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’14, San Diego, CA, USA, January 22–24, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2544-8). 569-581 (2014). MSC: 68N18 68N30 68N20 68Q60 PDFBibTeX XMLCite \textit{D. Zhang} and \textit{A. C. Myers}, in: Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '14, San Diego, CA, USA, January 22--24, 2014. New York, NY: Association for Computing Machinery (ACM). 569--581 (2014; Zbl 1284.68141) Full Text: DOI
Bodin, Martin; Chargueraud, Arthur; Filaretti, Daniele; Gardner, Philippa; Maffeis, Sergio; Naudziuniene, Daiva; Schmitt, Alan; Smith, Gareth A trusted mechanised JavaSript specification. (English) Zbl 1284.68381 Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’14, San Diego, CA, USA, January 22–24, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2544-8). 87-100 (2014). MSC: 68Q60 68N30 68T15 68N15 PDFBibTeX XMLCite \textit{M. Bodin} et al., in: Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '14, San Diego, CA, USA, January 22--24, 2014. New York, NY: Association for Computing Machinery (ACM). 87--100 (2014; Zbl 1284.68381) Full Text: DOI
Kobayashi, Naoki Model checking higher-order programs. (English) Zbl 1281.68157 J. ACM 60, No. 3, Article No. 20, 62 p. (2013). MSC: 68Q60 03B40 68N18 PDFBibTeX XMLCite \textit{N. Kobayashi}, J. ACM 60, No. 3, Article No. 20, 62 p. (2013; Zbl 1281.68157) Full Text: DOI
Im, Hyeonseung; Nakata, Keiko; Park, Sungwoo Contractive signatures with recursive types, type parameters, and abstract types. (English) Zbl 1335.68057 Fomin, Fedor V. (ed.) et al., Automata, languages, and programming. 40th international colloquium, ICALP 2013, Riga, Latvia, July 8–12, 2013, Proceedings, Part II. Berlin: Springer (ISBN 978-3-642-39211-5/pbk). Lecture Notes in Computer Science 7966, 299-311 (2013). MSC: 68N30 03B70 PDFBibTeX XMLCite \textit{H. Im} et al., Lect. Notes Comput. Sci. 7966, 299--311 (2013; Zbl 1335.68057) Full Text: DOI
Scherer, Gabriel; Rémy, Didier GADTs meet subtyping. (English) Zbl 1381.68060 Felleisen, Matthias (ed.) et al., Programming languages and systems. 22nd European symposium on programming, ESOP 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16–24, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-37035-9/pbk). Lecture Notes in Computer Science 7792, 554-573 (2013). MSC: 68N30 68N18 68Q65 PDFBibTeX XMLCite \textit{G. Scherer} and \textit{D. Rémy}, Lect. Notes Comput. Sci. 7792, 554--573 (2013; Zbl 1381.68060) Full Text: DOI arXiv
Filliâtre, Jean-Christophe; Paskevich, Andrei Why3 – where programs meet provers. (English) Zbl 1435.68366 Felleisen, Matthias (ed.) et al., Programming languages and systems. 22nd European symposium on programming, ESOP 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16–24, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 7792, 125-128 (2013). MSC: 68V15 68N30 68Q60 PDFBibTeX XMLCite \textit{J.-C. Filliâtre} and \textit{A. Paskevich}, Lect. Notes Comput. Sci. 7792, 125--128 (2013; Zbl 1435.68366) Full Text: DOI
Henry, Grégoire; Mauny, Michel; Chailloux, Emmanuel; Manoury, Pascal Typing unmarshalling without marshalling types. (English) Zbl 1291.68121 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, 287-298 (2012). MSC: 68N18 68N15 68Q65 PDFBibTeX XMLCite \textit{G. Henry} et al., 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). 287--298 (2012; Zbl 1291.68121) Full Text: DOI Link
Shved, P. E.; Mutilin, V. S.; Mandrykin, M. U. Experience of improving the BLAST static verification tool. (English. Russian original) Zbl 1252.68081 Program. Comput. Softw. 38, No. 3, 134-142 (2012); translation from Programmirovanie 38, No. 3 (2012). MSC: 68N30 PDFBibTeX XMLCite \textit{P. E. Shved} et al., Program. Comput. Softw. 38, No. 3, 134--142 (2012; Zbl 1252.68081); translation from Programmirovanie 38, No. 3 (2012) Full Text: DOI
Carlier, Matthieu; Dubois, Catherine; Gotlieb, Arnaud A certified constraint solver over finite domains. (English) Zbl 1372.68165 Giannakopoulou, Dimitra (ed.) et al., FM 2012: Formal methods. 18th international symposium, Paris, France, August 27–31, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32758-2/pbk). Lecture Notes in Computer Science 7436, 116-131 (2012). MSC: 68Q60 68T15 68T20 PDFBibTeX XMLCite \textit{M. Carlier} et al., Lect. Notes Comput. Sci. 7436, 116--131 (2012; Zbl 1372.68165) Full Text: DOI
Krishnaswami, Neelakantan R.; Benton, Nick A semantic model for graphical user interfaces. (English) Zbl 1323.68129 Proceedings of the 16th ACM SIGPLAN international conference on functional programming, ICFP ’11, Tokyo, Japan, September 19–21, 2011. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-0865-6). ACM SIGPLAN Notices 46, No. 9, 45-57 (2011). MSC: 68N18 03B70 68N30 68Q55 68U35 PDFBibTeX XMLCite \textit{N. R. Krishnaswami} and \textit{N. Benton}, in: Proceedings of the 16th ACM SIGPLAN international conference on functional programming, ICFP '11, Tokyo, Japan, September 19--21, 2011. New York, NY: Association for Computing Machinery (ACM). 45--57 (2011; Zbl 1323.68129) Full Text: DOI
Garrigue, Jacques; Nakata, Keiko Path resolution for nested recursive modules. (English) Zbl 1256.68032 High.-Order Symb. Comput. 24, No. 3, 207-237 (2011). MSC: 68N18 68N30 PDFBibTeX XMLCite \textit{J. Garrigue} and \textit{K. Nakata}, High.-Order Symb. Comput. 24, No. 3, 207--237 (2011; Zbl 1256.68032) Full Text: DOI
Bulwahn, Lukas Smart test data generators via logic programming. (English) Zbl 1245.68168 Gallagher, John P. (ed.) et al., Technical communications of the 27th international conference on logic programming (ICLP 2011), Lexington, Kentucky, USA, July 6–10, 2011. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-31-6). LIPIcs – Leibniz International Proceedings in Informatics 11, 139-150, electronic only (2011). MSC: 68T15 68N30 68N17 68N18 PDFBibTeX XMLCite \textit{L. Bulwahn}, LIPIcs -- Leibniz Int. Proc. Inform. 11, 139--150 (2011; Zbl 1245.68168) Full Text: DOI Link
Stratulat, Sorin; Demange, Vincent Automated certification of implicit induction proofs. (English) Zbl 1350.68245 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, 37-53 (2011). MSC: 68T15 68Q60 PDFBibTeX XMLCite \textit{S. Stratulat} and \textit{V. Demange}, Lect. Notes Comput. Sci. 7086, 37--53 (2011; Zbl 1350.68245) Full Text: DOI
Calvès, Christophe; Fernández, Maribel The first-order nominal link. (English) Zbl 1326.68083 Alpuente, María (ed.), Logic-based program synthesis and transformation. 20th international symposium, LOPSTR 2010, Hagenberg, Austria, July 23–25, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-20550-7/pbk). Lecture Notes in Computer Science 6564, 234-248 (2011). MSC: 68N30 PDFBibTeX XMLCite \textit{C. Calvès} and \textit{M. Fernández}, Lect. Notes Comput. Sci. 6564, 234--248 (2011; Zbl 1326.68083) Full Text: DOI
Lutteroth, Christof; Draheim, Dirk; Weber, Gerald A type system for reflective program generators. (English) Zbl 1215.68062 Sci. Comput. Program. 76, No. 5, 392-422 (2011). MSC: 68N19 68N30 PDFBibTeX XMLCite \textit{C. Lutteroth} et al., Sci. Comput. Program. 76, No. 5, 392--422 (2011; Zbl 1215.68062) Full Text: DOI
Carette, Jacques; Kiselyov, Oleg Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code. (English) Zbl 1215.68059 Sci. Comput. Program. 76, No. 5, 349-375 (2011). MSC: 68N19 68N30 PDFBibTeX XMLCite \textit{J. Carette} and \textit{O. Kiselyov}, Sci. Comput. Program. 76, No. 5, 349--375 (2011; Zbl 1215.68059) Full Text: DOI
Terauchi, Tachio Dependent types from counterexamples. (English) Zbl 1312.68041 Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’10, Madrid, Spain, January 17–23, 2010. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-479-9). 119-130 (2010). MSC: 68N18 68N30 68Q55 68Q60 PDFBibTeX XMLCite \textit{T. Terauchi}, in: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '10, Madrid, Spain, January 17--23, 2010. New York, NY: Association for Computing Machinery (ACM). 119--130 (2010; Zbl 1312.68041) Full Text: DOI Link
Marić, Filip Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL. (English) Zbl 1208.68205 Theor. Comput. Sci. 411, No. 50, 4333-4356 (2010). MSC: 68T20 68Q60 PDFBibTeX XMLCite \textit{F. Marić}, Theor. Comput. Sci. 411, No. 50, 4333--4356 (2010; Zbl 1208.68205) Full Text: DOI
Bird, Richard Pearls of functional algorithm design. (English) Zbl 1229.68026 Cambridge: Cambridge University Press (ISBN 978-0-521-51338-8/hbk; 978-0-511-79588-6/ebook). xii, 277 p. (2010). Reviewer: Haim Kilov (Millington) MSC: 68N18 68-02 68N30 68W40 68W05 PDFBibTeX XMLCite \textit{R. Bird}, Pearls of functional algorithm design. Cambridge: Cambridge University Press (2010; Zbl 1229.68026)
Armand, Michaël; Grégoire, Benjamin; Spiwack, Arnaud; Théry, Laurent Extending Coq with imperative features and its application to SAT verification. (English) Zbl 1291.68318 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, 83-98 (2010). MSC: 68T15 68Q60 PDFBibTeX XMLCite \textit{M. Armand} et al., Lect. Notes Comput. Sci. 6172, 83--98 (2010; Zbl 1291.68318) Full Text: DOI Link
Calvès, Christophe; Fernández, Maribel Matching and alpha-equivalence check for nominal terms. (English) Zbl 1206.68159 J. Comput. Syst. Sci. 76, No. 5, 283-301 (2010). MSC: 68Q42 68N30 PDFBibTeX XMLCite \textit{C. Calvès} and \textit{M. Fernández}, J. Comput. Syst. Sci. 76, No. 5, 283--301 (2010; Zbl 1206.68159) Full Text: DOI
Ridge, Thomas Verifying distributed systems: the operational approach. (English) Zbl 1315.68105 Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’09, Savannah, GA, USA, January 18–24, 2009. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-379-2). 429-440 (2009). MSC: 68N30 68N19 68M14 68Q60 68T15 PDFBibTeX XMLCite \textit{T. Ridge}, in: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '09, Savannah, GA, USA, January 18--24, 2009. New York, NY: Association for Computing Machinery (ACM). 429--440 (2009; Zbl 1315.68105) Full Text: DOI
Ellison, Chucky; Şerbănuţă, Traian Florin; Roşu, Grigore A rewriting logic approach to type inference. (English) Zbl 1253.68211 Corradini, Andrea (ed.) et al., Recent trends in algebraic development techniques. 19th international workshop, WADT 2008, Pisa, Italy, June 13–16, 2008. Revised selected papers. Berlin: Springer (ISBN 978-3-642-03428-2/pbk). Lecture Notes in Computer Science 5486, 135-151 (2009). MSC: 68Q55 68N30 68Q42 PDFBibTeX XMLCite \textit{C. Ellison} et al., Lect. Notes Comput. Sci. 5486, 135--151 (2009; Zbl 1253.68211) Full Text: DOI
Berghofer, Stefan; Bulwahn, Lukas; Haftmann, Florian Turning inductive into equational specifications. (English) Zbl 1252.68249 Berghofer, Stefan (ed.) et al., Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-03358-2/pbk). Lecture Notes in Computer Science 5674, 131-146 (2009). MSC: 68T15 68N17 68N18 68Q60 PDFBibTeX XMLCite \textit{S. Berghofer} et al., Lect. Notes Comput. Sci. 5674, 131--146 (2009; Zbl 1252.68249) Full Text: DOI
Bauer, Andrej; Stone, Christopher A. RZ: a tool for bringing constructive and computable mathematics closer to programming practice. (English) Zbl 1156.03301 J. Log. Comput. 19, No. 1, 17-43 (2009). MSC: 03-04 03F60 03F65 68N30 PDFBibTeX XMLCite \textit{A. Bauer} and \textit{C. A. Stone}, J. Log. Comput. 19, No. 1, 17--43 (2009; Zbl 1156.03301) Full Text: DOI Link
Bauer, Andrej; Kavkler, Iztok Implementing real numbers with RZ. (English) Zbl 1262.03076 Dilhage, R. (ed.) et al., Proceedings of the fourth international conference on computability and complexity in analysis (CCA 2007), Siena, Italy, June 16–18, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 202, 365-384 (2008). MSC: 03D78 68N30 68Q60 PDFBibTeX XMLCite \textit{A. Bauer} and \textit{I. Kavkler}, Electron. Notes Theor. Comput. Sci. 202, 365--384 (2008; Zbl 1262.03076) Full Text: DOI
Cécé, Gérard; Héam, Pierre-Cyrille; Mainier, Yann Efficiency of automata in semi-commutation verification techniques. (English) Zbl 1144.68039 Theor. Inform. Appl. 42, No. 2, 197-215 (2008). MSC: 68Q60 68N30 68Q45 PDFBibTeX XMLCite \textit{G. Cécé} et al., Theor. Inform. Appl. 42, No. 2, 197--215 (2008; Zbl 1144.68039) Full Text: DOI EuDML HAL
Rideau, Laurence; Serpette, Bernard Paul; Leroy, Xavier Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves. (English) Zbl 1140.68491 J. Autom. Reasoning 40, No. 4, 307-326 (2008). MSC: 68T15 68N20 68Q60 PDFBibTeX XMLCite \textit{L. Rideau} et al., J. Autom. Reasoning 40, No. 4, 307--326 (2008; Zbl 1140.68491) Full Text: DOI Link
Schwinghammer, J. On normalization by evaluation for object calculi. (English) Zbl 1138.68350 Miculan, Marino (ed.) et al., Types for proofs and programs. International conference, TYPES 2007, Cividale des Friuli, Italy, May 2–5, 2007. Revised selected papers. Berlin: Springer (ISBN 978-3-540-68084-0/pbk). Lecture Notes in Computer Science 4941, 173-187 (2008). MSC: 68N18 68N30 PDFBibTeX XMLCite \textit{J. Schwinghammer}, Lect. Notes Comput. Sci. 4941, 173--187 (2008; Zbl 1138.68350) Full Text: DOI
Kiselyov, Oleg; Shan, Chung-chieh Lightweight static capabilities. (English) Zbl 1277.68052 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, 79-104 (2007). MSC: 68N19 68N18 68Q60 PDFBibTeX XMLCite \textit{O. Kiselyov} and \textit{C.-c. Shan}, Electron. Notes Theor. Comput. Sci. 174, No. 7, 79--104 (2007; Zbl 1277.68052) Full Text: DOI
Bauer, Andrej; Stone, Christopher A. RZ: A tool for bringing constructive and computable mathematics closer to programming practice. (English) Zbl 1150.03300 Cooper, S. Barry (ed.) et al., Computation and logic in the real world. Third conference on computability in Europe, CiE 2007, Siena, Italy, June 18–23, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73000-2/pbk). Lecture Notes in Computer Science 4497, 28-42 (2007). MSC: 03-04 03F60 03F65 68N30 PDFBibTeX XMLCite \textit{A. Bauer} and \textit{C. A. Stone}, Lect. Notes Comput. Sci. 4497, 28--42 (2007; Zbl 1150.03300) Full Text: DOI
Allamigeon, Xavier; Godard, Wenceslas; Hymans, Charles Static analysis of string manipulations in critical embedded C programs. (English) Zbl 1225.68064 Yi, Kwangkeun (ed.), Static analysis. 13th international symposium, SAS 2006, Seoul, Korea, August 29–31, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-37756-6/pbk). Lecture Notes in Computer Science 4134, 35-51 (2006). MSC: 68N30 68Q55 PDFBibTeX XMLCite \textit{X. Allamigeon} et al., Lect. Notes Comput. Sci. 4134, 35--51 (2006; Zbl 1225.68064) Full Text: DOI
Harrison, John Verification: industrial applications. (English) Zbl 1129.68447 Schwichtenberg, Helmut (ed.) et al., Proof technology and computation. Papers from the summer school, Marktoberdorf, Germany, July 29–August 10, 2003. Amsterdam: IOS Press (ISBN 1-58603-625-4/hbk). NATO Science Series III: Computer & Systems Sciences 200, 161-205 (2006). MSC: 68Q60 68T15 PDFBibTeX XMLCite \textit{J. Harrison}, NATO Sci. Ser. III, Comput. Syst. Sci. 200, 161--205 (2006; Zbl 1129.68447)
Hymans, Charles Verification of an error correcting code by abstract interpretation. (English) Zbl 1111.68507 Cousot, Radhia (ed.), Verfication, model checking, and abstract interpretation. 6th international conference, VMCAI 2005, Paris, France, January 17–19, 2005. Proceedings. Berlin: Springer (ISBN 3-540-24297-X/pbk). Lecture Notes in Computer Science 3385, 330-345 (2005). MSC: 68Q60 94B15 94B50 PDFBibTeX XMLCite \textit{C. Hymans}, Lect. Notes Comput. Sci. 3385, 330--345 (2005; Zbl 1111.68507) Full Text: DOI
Gurevich, Yuri; Rossman, Benjamin; Schulte, Wolfram Semantic essence of AsmL. (English) Zbl 1077.68052 Theor. Comput. Sci. 343, No. 3, 370-412 (2005). MSC: 68Q60 68Q55 PDFBibTeX XMLCite \textit{Y. Gurevich} et al., Theor. Comput. Sci. 343, No. 3, 370--412 (2005; Zbl 1077.68052) Full Text: DOI
Cachera, David; Jensen, Thomas; Pichardie, David; Rusu, Vlad Extracting a data flow analyser in constructive logic. (English) Zbl 1077.68051 Theor. Comput. Sci. 342, No. 1, 56-78 (2005). MSC: 68Q60 68Q55 68T15 PDFBibTeX XMLCite \textit{D. Cachera} et al., Theor. Comput. Sci. 342, No. 1, 56--78 (2005; Zbl 1077.68051) Full Text: DOI
Cachera, David; Jensen, Thomas; Pichardie, David; Rusu, Vlad Extracting a data flow analyser in constructive logic. (English) Zbl 1126.68345 Schmidt, David (ed.), Programming languages and systems. 13th European symposium on programming, ESOP 2004, held as part of the joint European conferences on theory and practice of software, ETAPS 2004, Barcelona, Spain, March 29 – April 2, 2004. Proceedings. Berlin: Springer (ISBN 3-540-21313-9/pbk). Lecture Notes in Computer Science 2986, 385-400 (2004). MSC: 68N30 03B70 PDFBibTeX XMLCite \textit{D. Cachera} et al., Lect. Notes Comput. Sci. 2986, 385--400 (2004; Zbl 1126.68345) Full Text: DOI
Filliâtre, Jean-Christophe; Letouzey, Pierre Functors for proofs and programs. (English) Zbl 1126.68475 Schmidt, David (ed.), Programming languages and systems. 13th European symposium on programming, ESOP 2004, held as part of the joint European conferences on theory and practice of software, ETAPS 2004, Barcelona, Spain, March 29 – April 2, 2004. Proceedings. Berlin: Springer (ISBN 3-540-21313-9/pbk). Lecture Notes in Computer Science 2986, 370-384 (2004). MSC: 68Q60 68P05 PDFBibTeX XMLCite \textit{J.-C. Filliâtre} and \textit{P. Letouzey}, Lect. Notes Comput. Sci. 2986, 370--384 (2004; Zbl 1126.68475) Full Text: DOI
Atanassow, Frank; Jeuring, Johan Inferring type isomorphisms generically. (English) Zbl 1106.68337 Kozen, Dexter (ed.), Mathematics of program construction. 7th international conference, MPC 2004, Stirling, Scotland, UK, July 12–14, 2004. Proceedings. Berlin: Springer (ISBN 3-540-22380-0/pbk). Lecture Notes in Computer Science 3125, 32-53 (2004). MSC: 68N30 68N18 PDFBibTeX XMLCite \textit{F. Atanassow} and \textit{J. Jeuring}, Lect. Notes Comput. Sci. 3125, 32--53 (2004; Zbl 1106.68337) Full Text: DOI
Kreitz, Christoph Building reliable, high-performance networks with the Nuprl proof development system. (English) Zbl 1083.68010 J. Funct. Program. 14, No. 1, 21-68 (2004). MSC: 68M20 68N18 68Q60 68T15 PDFBibTeX XMLCite \textit{C. Kreitz}, J. Funct. Program. 14, No. 1, 21--68 (2004; Zbl 1083.68010) Full Text: DOI
Fournet, Cédric; Laneve, Cosimo; Maranget, Luc; Rémy, Didier Inheritance in the join calculus. (English) Zbl 1035.03011 J. Log. Algebr. Program. 57, No. 1-2, 23-69 (2003). MSC: 03B70 68Q85 68N30 PDFBibTeX XMLCite \textit{C. Fournet} et al., J. Log. Algebr. Program. 57, No. 1--2, 23--69 (2003; Zbl 1035.03011) Full Text: DOI
Grégoire, Benjamin; Leroy, Xavier A compiled implementation of strong reduction. (English) Zbl 1322.68053 Proceedings of the 7th ACM SIGPLAN international conference on functional programming, ICFP ’02, Pittsburgh, PA, USA, October 4–6, 2002. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-58113-487-8). ACM SIGPLAN Notices 37, No. 9, 235-246 (2002). MSC: 68N30 68N18 68Q60 68T15 PDFBibTeX XMLCite \textit{B. Grégoire} and \textit{X. Leroy}, in: Proceedings of the 7th ACM SIGPLAN international conference on functional programming, ICFP '02, Pittsburgh, PA, USA, October 4--6, 2002. New York, NY: Association for Computing Machinery (ACM). 235--246 (2002; Zbl 1322.68053) Full Text: DOI HAL
Glynn, Kevin; Stuckey, Peter J.; Sulzmann, Martin; Søndergaard, Harald Exception analysis for non-strict languages. (English) Zbl 1322.68041 Proceedings of the 7th ACM SIGPLAN international conference on functional programming, ICFP ’02, Pittsburgh, PA, USA, October 4–6, 2002. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-58113-487-8). ACM SIGPLAN Notices 37, No. 9, 98-109 (2002). MSC: 68N18 68N15 68N20 68N30 PDFBibTeX XMLCite \textit{K. Glynn} et al., in: Proceedings of the 7th ACM SIGPLAN international conference on functional programming, ICFP '02, Pittsburgh, PA, USA, October 4--6, 2002. New York, NY: Association for Computing Machinery (ACM). 98--109 (2002; Zbl 1322.68041) Full Text: DOI
Syme, Don; Gordon, Andrew D. Automating type soundness proofs via decision procedures and guided reductions. (English) Zbl 1023.68539 Baaz, Matthias (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 9th international conference, LPAR 2002, Tbilisi, Georgia, October 14-18, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2514, 418-434 (2002). MSC: 68N30 68T15 PDFBibTeX XMLCite \textit{D. Syme} and \textit{A. D. Gordon}, Lect. Notes Comput. Sci. 2514, 418--434 (2002; Zbl 1023.68539) Full Text: Link
Fisher, Kathleen; Reppy, John Inheritance-based subtyping. (English) Zbl 1012.68044 Inf. Comput. 177, No. 1, 28-55 (2002). MSC: 68N19 68Q65 PDFBibTeX XMLCite \textit{K. Fisher} and \textit{J. Reppy}, Inf. Comput. 177, No. 1, 28--55 (2002; Zbl 1012.68044) Full Text: DOI Link
Danvy, Olivier; Grobauer, Bernd; Rhiger, Morten A unifying approach to goal-directed evaluation. (English) Zbl 1030.68542 Taha, Walid (ed.), Semantics, applications, and implementation of program generation. 2nd international workshop, SAIG 2001, Florence, Italy, September 6, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2196, 108-125 (2001). MSC: 68N30 68N15 68N20 PDFBibTeX XMLCite \textit{O. Danvy} et al., Lect. Notes Comput. Sci. 2196, 108--125 (2001; Zbl 1030.68542) Full Text: Link
Tews, Hendrik Coalgebras for binary methods: Properties of bisimulations and invariants. (English) Zbl 0983.68126 Theor. Inform. Appl. 35, No. 1, 83-111 (2001). MSC: 68Q65 68N19 03G30 68Q55 PDFBibTeX XMLCite \textit{H. Tews}, Theor. Inform. Appl. 35, No. 1, 83--111 (2001; Zbl 0983.68126) Full Text: DOI Numdam EuDML Link
Rothe, Jan; Tews, Hendrik; Jacobs, Bart The coalgebraic class specification language CCSL. (English) Zbl 0970.68104 J. UCS 7, No. 2, Spec. Iss., 175-193 (2001). MSC: 68Q60 68T27 PDFBibTeX XMLCite \textit{J. Rothe} et al., J. UCS 7, No. 2, 175--193 (2001; Zbl 0970.68104)
Delahaye, David Information retrieval in a Coq proof library using type isomorphisms. (English) Zbl 0988.68542 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, 131-147 (2000). MSC: 68N30 68P20 03B40 PDFBibTeX XMLCite \textit{D. Delahaye}, Lect. Notes Comput. Sci. 1956, 131--147 (2000; Zbl 0988.68542)
Fisher, Kathleen; Reppy, John; Riecke, Jon G. A calculus for compiling and linking classes. (English) Zbl 0971.68575 Smolka, Gerd (ed.), Programming languages and systems. 9th European symposium on programming, ESOP 2000. Held as part of the joint European conferences on theory and practice of software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1782, 135-149 (2000). MSC: 68U99 68N15 68N30 PDFBibTeX XMLCite \textit{K. Fisher} et al., Lect. Notes Comput. Sci. 1782, 135--149 (2000; Zbl 0971.68575)