Tiago Cogumbreiro @AssertionError@types.pl
Computer Scientist researching verification of parallel programming languages (CUDA).
I play around with: #typesystems for #concurrency, #behavioraltypes for the #SPMD programming model, mechanized proofs in #coq, tools implemented in #OCaml. I design tools for CS Education.
Assistant professor @ UMass Boston
Joined Nov 2022
Pinned toot
Hi types.pl,
I am a computer scientist interested in #verification, concurrency theory applied to parallel systems.
My main research project deals with verifying safety and performance properties of #CUDA kernels.
I write code for research mainly in #OCaml and #Coq.
I am passionate about teaching. I am currently using Racket to teach functional programming and Coq to teach Intro to Theory of Computation.
I use this to share my own research findings, papers I like, and software that I find fun.
PS: I just migrated from mathstodon.xyz and I think I lost my posts.
Tiago Cogumbreiro
boosted
Two updates about the 16th Interaction and Concurrency Experience (ICE 2023) workshop:
1. We are thrilled to announce that Adrian Francalanza (https://staff.um.edu.mt/afra1/) has accepted to be our first guest speaker, and
2. The deadlines have been extended by ~2 weeks.
Check out https://www.discotec.org/2023/ice !
Tiago Cogumbreiro
boosted
#CallForContributions #ThEdu23 (Theorem proving components for Educational software) "brings together experts in automated deduction with experts in education in order to further clarify the shape of a new software generation and to discuss existing systems" https://www.uc.pt/en/congressos/thedu/ThEdu23/cfp #ATP #CSEd #CSEducation
Tiago Cogumbreiro
boosted
Really pleased to have pushed watch.ocaml.org out of beta. 130+ videos about #ocaml dating back to 2010 (and would like to get more historical ones) all available via PeerTube/ActivityPub. https://discuss.ocaml.org/t/watch-ocaml-org-out-of-beta-and-a-call-for-new-videos/11561
Tiago Cogumbreiro
boosted
The Center for Integrated Research Computing (CIRC) at the University of Rochester is seeking a computational scientist:
https://ps.its.rochester.edu/psp/PSApplyOnline/EMPLOYEE/HRMS/c/HRS_HRAM_FL.HRS_CG_SEARCH_FL.GBL?Page=HRS_APP_JBPST_FL&Action=U&FOCUS=Applicant&SiteId=1&JobOpeningId=243101&PostingSeq=1
https://ps.its.rochester.edu/psp/PSApplyOnline/EMPLOYEE/HRMS/c/HRS_HRAM_FL.HRS_CG_SEARCH_FL.GBL?Page=HRS_APP_JBPST_FL&Action=U&FOCUS=Applicant&SiteId=1&JobOpeningId=243101&PostingSeq=1
Teaching my first module in #TypedRacket this semester: thunks and promises, with a hint of polymorphism.
So far, I really enjoyed the language. I love that using TypedRacket code in Racket is so seamless. Types being contracts just feels so good.
My biggest surprise right now is pattern matching with "match" https://racket.discourse.group/t/pattern-matching-in-typedracket-that-uses-types-to-rule-out-impossible-branches/1743
Tiago Cogumbreiro
boosted
I am currently looking for #PhD and #post-doc candidates to work with me in #Augusta (GA, USA) on formal methods for #concurrent #reversible programs. More info at https://spots.augusta.edu/caubert/research/cinrc/phd_ad.html #Academia #job
To appear in FMSD'23: *Memory Access Protocols:
Certified Data-Race Freedom
for #GPU Kernels*. Key new points vs our CAV21 publication: full discussion of Coq proofs, cleaned up definitions, gentler introduction of the defs+examples.
Note to self, the expression x <= y is written in Prolog as x =< y, even though x >= y is written as x >= y. Something something parsing?
Note to self: with 2FA, my phone should not be the only way to authenticate. I bought a new phone and almost locked myself out of my school's authentication castle.
Tiago Cogumbreiro
boosted
Property-based testing stateful systems: a tutorial. ~ Stevan Andjelkovic. https://github.com/stevana/property-based-testing-stateful-systems-tutorial/tree/47b5b141b45cc484f8a6cfbff0d38aeceac7ca6d#readme #Haskell #FunctionalProgramming
Tiago Cogumbreiro
boosted
If you're using Holbert in the classroom, please tell us! So far, I'm aware of two classes in which it is/will be actively used and two more where instructors tell me they plan to use it at some point but haven't developed the materials yet.
Tiago Cogumbreiro
boosted
New #Futhark mugs. We hand out these to students who get a top grade in our parallel programming courses.
Tiago Cogumbreiro
boosted
Happy to release the first version of smlfmt, a formatter for Standard ML.
https://github.com/shwestrick/smlfmt/releases/tag/v1.0.0
This has been a hobby project for a while now -- I remember starting work on the parser while visiting my sister for Thanksgiving in 2020. Back then, I was just curious about parsing and wanted to give it a shot. But then a few folks from CMU got interested in the project and suggested that we could turn it into a code formatter. Big thanks to all the Project Savannah folks for your contributions, suggestions, and support!
I had a great time working on this over winter break. Now it's time to get back to research!
Tiago Cogumbreiro
boosted
Holbert 0.5.1 has been released! Many minor things have been improved, but highlights are:
- Footnote/reference popups
- Links and image embedding (not added to help yet)
- A basic presentation mode that shows a document as a slideshow
- Auto-renames variables in goals to avoid confusing shadows
- Very basic infix input syntax support using "Notation", but does not yet support associativity or precedence settings.
http://liamoc.net/holbert/
Tiago Cogumbreiro
boosted
After a slight delay due to winter holidays, the December release of Functional Programming in Lean is out, featuring a new chapter on applicative functors:
https://leanprover.github.io/functional_programming_in_lean/
Tiago Cogumbreiro
boosted
OOH Look what I found: "Program Proofs" by Leino arriving 2023 [on Dafny]:
https://mitpress.mit.edu/9780262546232/program-proofs/
https://mitpress.mit.edu/9780262546232/program-proofs/
Follow up: the winning logic parameters in terms of more answers given and also in terms of faster answers as an aggregate were AUFLIRA and AUFNIRA. This is surprising to me, since the formula we generate do not have arrays.
- AUFLIRA: "Closed linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value. "
- AUFNIRA: "Closed formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value. "
I love learning more about the subtleties of SAT solving. In one of our analysis, we are maximizing a numeric expression and we wanted add support for bit-vectors. The solver (Z3) started giving weird answers only when using bit-vector numerals. The problem is that maximization has no notion of bit-vector signedness.
StackOverflow was invaluable as usual:
https://stackoverflow.com/questions/64484347/optimize-signed-bitvectors-in-z3
Tiago Cogumbreiro
boosted
"Tools for checking and writing non-trivial DWARF programs"
😮
Varying the #Z3 logic parameter to see what works best in our DRF analysis.
Computer Scientist researching verification of parallel programming languages (CUDA).
I play around with: #typesystems for #concurrency, #behavioraltypes for the #SPMD programming model, mechanized proofs in #coq, tools implemented in #OCaml. I design tools for CS Education.
Assistant professor @ UMass Boston
Joined Nov 2022
