Name: Joao F. Ferreira
Type: User
Company: Instituto Superior Técnico & INESC-ID
Bio: Computer Scientist / CS Professor at Instituto Superior Técnico (University of Lisbon). Researcher at @inesc-id.
Twitter: jff
Location: Lisbon, Portugal
Blog: https://joaoff.com
Joao F. Ferreira's Projects
Repository for PDD 2013/2014
The CompCert formally-verified C compiler
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Dafny is a verification-aware programming language
Literate Haskell module with functions to enumerate the elements of the Eisenstein array. Also, we provide a program that searches for occurrences of the Eisenstein array on OEIS. (Joint work with Roland Backhouse.)
FME Teaching Committee
Offline Documentions for HandyControl
Examples of programs verified with HIP/SLEEK
A Twitter Client
A development of a subset of intuitionistic linear logic, suitable for representing narratives.
The MathSpad Editor
Python class implementing the algorithm that I and Roland Backhouse created in 2008 to enumerate the positive rational numbers in two different ways.
The Enterprise-ready testing and specification framework.
Example Streamlit app that you can fork to test out share.streamlit.io
Tests with Streams
TeLLer is a collection of tools that explore the use of linear logic applied to narrative generation and story telling.
Haskell binding to Google's AJAX Language API for Translation and Detection
A literate Haskell program that proves the inexistence of a unique existential binary operator
在线白板 Online whiteboard