En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado cómo trabajar con tablas en Haskell usando el módulo Data.Array.
Las transparencias usadas en la clase son las 18 primeras del tema 18:
Read More “I1M2012: Las tablas en Haskell”
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Developing an auction theory toolbox.
Sus autores son Christoph Lange, Colin Rowat, Wolfgang Windsteiger y Manfred Kerber.
Su resumen es
Auctions allocate trillions of dollars in goods and services every year. Auction design can have significant consequences, but its practice outstrips theory. We seek to advance auction theory with help from mechanised reasoning. To that end we are developing a toolbox of formalised representations of key facts of auction theory, which will allow auction designers to have relevant properties of their auctions machine-checked. As a first step, we are investigating the suitability of different mechanised reasoning systems (Isabelle, Theorema, and TPTP) for reproducing a key result of auction theory: Vickrey’s celebrated 1961 theorem on the properties of second price auctions – the foundational result in modern auction theory. Based on our formalisation experience, we give tentative recommendations on what system to use for what purpose in auction theory, and outline further steps towards a complete auction theory toolbox.
El trabajo se presentó en la AISB Convention 2013.
Los códigos de las correspondientes teorías se encuentran Auction Theory Toolbox (ATT). Contiene los códigos de las formalizaciones en CASL, Isabelle, Mizar y Theorema.
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Formalization of incremental simplex algorithm by stepwise refinement.
Sus autores son Mirko Spasić and Filip Marić (de la Universidad de Belgrado).
Su resumen es
We present an Isabelle/HOL formalization and total correctness proof for the incremental version of the Simplex algorithm which is used in most state-of-the-art SMT solvers. Formalization relies on stepwise program and data refinement, starting from a simple specification, going through a number of fine refinement steps, and ending up in a fully executable functional implementation. Symmetries present in the algorithm are handled with special care.
El trabajo se presentó en el FM2012 (18th International Symposium on Formal Methods) y las transparencias de la presentación se encuentran aquí.
El código de las teorías en Isabelle/HOL se encuentran aquí.
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre metalógica titulado Coinductive pearl: Modular first-order logic completeness.
Sus autores son Jasmin Christian Blanchette, Andrei Popescu y Dmitriy Traytel (de la Universidad Técnica de Munich).
Su resumen es
Codatatypes are unfortunately still missing in many programming languages and proof assistants. We make a case for their usefulness by revisiting a classic result: the completeness theorem for first-order logic established through a Gentzen system. Codatatypes help capture the essence of the proof, which establishes an abstract property of derivation trees independently of the concrete syntax or inference rules. This separation of concerns simplifies the presentation, especially for readers acquainted with lazy data structures. The proof is formalized in Isabelle/HOL and demonstrates the recently introduced definitional package for codatatypes and its integration with Isabelle’s Haskell code generator.
El código de las teorías Isabelle correspodientes se encuentra aquí.
Se ha publicado un artículo sobre la ensñanza de Haskell titulado Experience report: Teaching Haskell to the masses.
Sus autores son Jasmin Christian Blanchette, Tobias Nipkow, Lars Noschinski y Dmitriy Traytel (de la Universidad Técnica de Munich).
Su resumen es
We report on our experience teaching a Haskell-based functional programming course to over 600 students. The syllabus was organized around selected material from various sources. Throughout the term, we emphasized correctness through QuickCheck tests and proofs by induction. The submission architecture was coupled with automatic testing, giving students the possibility to correct mistakes before the deadline. To motivate the students, we complemented the weekly assignments with an informal competition.