- Xavier Leroy's publications
- https://xavierleroy.org/research.html
- this site is a GOLD MINE of information on type systems!!!
- https://xavierleroy.org/research.html
- Chris Lattner's PhD thesis: "LLVM: An Infrastructure for Multi-Stage Optimization" http://llvm.org/pubs/2002-12-LattnerMSThesis.html
- my good old bookmarked page: http://blog.fogus.me/2011/09/08/10-technical-papers-every-programmer-should-read-at-least-twice/
- http://canonical.org/~kragen/memory-models/
- there are some nice references in [Vorobyov], check them out!
- D EUTSCH , A.: Static verification of dynamic properties. for example
- "Software Foundations" books by Penn
- learn basic OCaml / Haskell to really get a feel for their type systems
- look at these, maybe you'll find some type checking related stuff:
- read this: https://blog.wesleyac.com/posts/language-todos
- intro to theorem proving: https://news.ycombinator.com/item?id=19659582
- "Rust: beyond the typechecker": https://blog.merigoux.ovh/en/2019/04/16/verifying-rust.html
- John Hopkins University course: Principles of programming languages
- what errors are NOT type errors?
- https://github.com/tompollard/phd_thesis_markdown
- Citation Style Language
- markdown title page templates:
- LATEX
- konténerizáció
- sérülékenység típusok
- security-vel kapcsolatos technológiák fejlődése
- egy meeting közben jutott eszembe a cégnél. Mit akartam ezzel?
- elmaradottak a hardware-es eszközök?
- segíthet rajtuk fejlettebb típusrendszerek használata?
- megvizsgálni a népszerű hardware leíró nyelveket
- hol tartanak a magas szintű programnyelvekhez képest?
- mik az elvárások egyikkel/másikkal szemben?
- lehetőségek?
- reconfigure.io?
- http://insights.sigasi.com/opinion/lacking-open-source-vhdl-simulator.html
on writing a language from scratch: - https://medium.freecodecamp.org/the-programming-language-pipeline-91d3f449c919
http://www.cse.chalmers.se/edu/year/2015/course/DAT150/lectures/proglang-07.html
google this !!: "Static vs. dynamic type systems: an empirical study about the relationship between type casts and development time pdf" - so many pdf results!
http://learnyouanagda.liamoc.net/pages/introduction.html
\pagebreak
Megjegyzés a tisztelt bíráló bizottságnak: A dolgozatom jelen állapota egy köztes állapot, több helyen tartalmaz feljegyzéseket, jelöléseket a további munkához. A terület, amit választottam nagyobb, érdekesebb, mint először gondoltam, jóval több tájékozódást és munkát igényel a részemről, mint számítottam, viszont szándékomban áll mélységében áttekinteni és a hiányzó részeket kidolgozni. A hiányzó fejezeteket a következő időszakban illetve a Szakdolgozat II. tágy keretein belül fogom befejezni.
https://pl.cs.jhu.edu/pl/book/book.pdf https://book.huihoo.com/programming-languages/book/html/main.html#mainli1.html
https://github.com/jozefg/learn-tt
links at bottom of github readme: - https://github.com/jozefg/learn-tt#learn-tt
This is incredible... many of the researchers I cited in my thesis have given lectures here!
https://seamk.libguides.com/instructionsforbachelorsthesis/thesisprocessandstructure
http://tomasp.net/blog/2015/against-types/
https://people.inf.elte.hu/pgj/nytr_msc/ https://www.inf.elte.hu/dstore/document/788/Kaposi_Ambrus_Nyelvek%20t%C3%ADpusrendszere_jegyzet_2017.pdf https://akaposi.github.io/hott_bevezeto.pdf
https://stackoverflow.com/a/38768279/1772429
https://www.youtube.com/watch?v=oPVTNxiMcSU https://speakerdeck.com/igstan/lets-write-a-type-checker
=== IDEA: create small programs for each concept in this section instead of examining languages at Section II separately!
- example of a type systems feature
- what would happen if such feature were missing from the language? === === ===
hagyjuk, ha nem muszáj!
- Static type checking can measurably increase programmer productivity. TODO: Likely false, there seems to be no evidence
- Using statically typed languages results in more reliable software.
- Despite their advantages, languages featuring advanced type systems are rarely used in the industry because of cultural reasons.
\pagebreak
TODO: get some ideas from this: "The Unreasonable Effectiveness of Dynamic Typing for Practical Programs"
https://lexi-lambda.github.io/blog/2020/01/19/no-dynamic-type-systems-are-not-inherently-more-open/ https://softwareengineering.stackexchange.com/questions/333643/what-is-a-type-system https://thevaluable.dev/type-system-explained/
RTTI is used in the context of some statically typed languages like C++. It means that some information about an object's type is made available to the programmer during run-time.
- dynamic casts - downcasting https://stackoverflow.com/a/2254183/1772429
- maybe a note about static casts - "static downcast" is undefined behavior https://stackoverflow.com/a/47310910/1772429
TODO: C++: dynamic_cast, typeid | Java: instanceof TODO: RTTI and Reflection slides: https://www.cs.huji.ac.il/course/2004/ood/docs/lec08.pdf TODO: connection between RTTI and reflection
Abstraction is the principle of reducing something to its essential characteristics, removing everything that is unnecessary to accurately represent it for a particular usage. Abstraction reduces complexity and increases efficiency. [@whatis-abstraction]
TODO: see "Types, abstraction and parametric polymorphism" paper in thesis_papers dir
TODO: summarize CAR Hoare's presentation on NullPointerExceptions (The Billion Dollar Mistake - 2009)
- https://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare
- 31:10 great notes about what to expect from programming languages
- 31:40 "formal verification"
- 37:34 "now, the real commercial imperative which requires greater attention paid to formal correctness of the programs is the virus."
- "it reaches paths of your program that normal execution never reaches"
- "it's no longer adequate to test your program against all the cases that are likely to arise..."
- 50:00 great thoughts about the
jmpmachine instruction
https://medium.com/@yuhuan/covariance-and-contravariance-in-java-6d9bfb7f6b8e https://blog.daftcode.pl/csi-python-type-system-episode-1-1c2ee1f8047c https://blog.daftcode.pl/csi-python-type-system-episode-2-baf5168038c0 https://en.wikipedia.org/wiki/Covariance_and_contravariance_(computer_science) https://en.wikipedia.org/wiki/Covariant_return_type
The next step for a programming langage with regards to type systems would be to define certain basic types and operations for the values in the program. These help reduce the cognitive load on the programmer and make it possible to check (either statically or dynamicall) whether some operation later in the code is considered legal or not. Today we take for granted such a type system but this indeed is a language feature that wasn't there for the first generations of computer programmers.
TODO: Explain why assembly has no types! Are there any advantages of not having types?
Typed Assembly Language papers (from around 1999) - Morrisett et al. - http://www.cs.cornell.edu/talc/papers.html - https://www.cs.princeton.edu/~dpw/papers/tal-toplas.pdf - https://www.cis.upenn.edu/~stevez/papers/MCGG99.pdf
TODO: read all of these! good material!
- https://cs.stackexchange.com/a/40098/30429
- https://softwareengineering.stackexchange.com/a/401220/90623
Agda: https://plfa.github.io/
TODO: revise after having tried such a language!
- solving injection with a type system
- security and modern type systems
TODO: stanford lecture notes on Memory Safety: https://stanford-cs242.github.io/f19/lectures/06-2-memory-safety.html TODO: the linked paper: "affine type system": https://gankra.github.io/blah/linear-rust/ TODO: nice paper: https://sergio.bz/docs/rusty-types-2016.pdf
https://stackoverflow.com/questions/2507766/merge-convert-multiple-pdf-files-into-one-pdf