Lecturas del Grupo de Lógica Computacional (del 8 al 15 de junio)
Esta entrada es una recopilación de lecturas compartidas esta semana (del 8 al 15 de junio) en la lista de correo del grupo de lógica computacional
La recopilación está ordenada por la fecha de su publicación en Twitter. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.
- La sémantique, c’est romantique (Sémantique des preuves et des programmes et mathématiques certifiées). ~ P. Pansu
- Is this a proof? (Seeking the limits of mathematical proofs). ~ D. Lipton & K. Regan
- Social processes and proofs of theorems and programs. ~ R.A. De Millo, R.J. Lipton & A.J. Perlis #Proofs
- Social processes, program verification and all that. ~ A. Asperti, H. Geuvers & R. Natarajan. #Proofs
- Proof, message and certificate. ~ A. Asperti #Proofs
- Computers and the sociology of mathematical proof. ~ D. MacKenzie #Proofs
- Boolean expression checkers. ~ T. Nipkow #AFP #Isabelle_HOL
- Evaluating Haskell expressions in a tutoring environment. ~ T. Olmer, B. Heeren & J. Jeuring #Haskell
- Flipped graduate classroom in a Haskell-based software testing course. ~ J. van Eijck & V. Zaytsev #Haskell
- Verified networking using dependent types. ~ S. Fowler #Idris
- NLCertify: A tool for formal nonlinear optimization. ~ V. Magron #Coq
- Haxl, el framework Haskell para acceder a datos. ~ E. Goette #Haskell
- Applications of SMT solvers to program verification. ~ N. Bjørner & L. de Moura #SMT
- Set theory or higher order logic to represent auction concepts in Isabelle? ~ M.B. Caminati et als. #Isabelle_HOL
- Spreadsheet-like programming in Haskell. ~ G. Gonzalez #Haskell
- Computerising mathematical text. ~ F. Kamareddine et als.