jff
Computer Scientist / CS Professor at Instituto Superior Técnico (University of Lisbon). Researcher at @inesc-id.
Instituto Superior Técnico & INESC-IDLisbon, Portugal
Pinned Repositories
eisenstein
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.)
hip-examples
Examples of programs verified with HIP/SLEEK
mathspad
The MathSpad Editor
rationals-python
Python class implementing the algorithm that I and Roland Backhouse created in 2008 to enumerate the positive rational numbers in two different ways.
streams
Tests with Streams
TeLLer
TeLLer is a collection of tools that explore the use of linear logic applied to narrative generation and story telling.
translate
Haskell binding to Google's AJAX Language API for Translation and Detection
ueq-binary-op
A literate Haskell program that proves the inexistence of a unique existential binary operator
smartbugs
SmartBugs: A Framework to Analyze Ethereum Smart Contracts
smartbugs-wild
This repository contains 47,398 smart contracts extracted from the Ethereum network.
jff's Repositories
jff/TeLLer
TeLLer is a collection of tools that explore the use of linear logic applied to narrative generation and story telling.
jff/eisenstein
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.)
jff/streams
Tests with Streams
jff/mathspad
The MathSpad Editor
jff/rationals-python
Python class implementing the algorithm that I and Roland Backhouse created in 2008 to enumerate the positive rational numbers in two different ways.
jff/translate
Haskell binding to Google's AJAX Language API for Translation and Detection
jff/hip-examples
Examples of programs verified with HIP/SLEEK
jff/Hotot
A Twitter Client
jff/ueq-binary-op
A literate Haskell program that proves the inexistence of a unique existential binary operator
jff/1314-TEES-PDD
Repository for PDD 2013/2014
jff/CompCert
The CompCert formally-verified C compiler
jff/coq
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.
jff/dafny
Dafny is a verification-aware programming language
jff/DataUsageCheck-FBInfer
jff/donate
jff/fme-teaching
FME Teaching Committee
jff/HandyDoc
Offline Documentions for HandyControl
jff/humanaethica
jff/ill_narratives
A development of a subset of intuitionistic linear logic, suitable for representing narratives.
jff/sarif-test
jff/spock
The Enterprise-ready testing and specification framework.
jff/streamlit-example
Example Streamlit app that you can fork to test out share.streamlit.io
jff/XBoard
在线白板 Online whiteboard