Progress in Programming Language Semantics Frameworks /
Představa masové produkce počítačového software bez použití vysokoúrovňových programovacích jazyků je obtížná. Tyto jazyky odstiňují softwarové inženýry od detailů přítomných v moderních počítačových architekturách: instrukční sady, keše, provádění instrukcí mimo pořadí, a tak dále. Ale když se abst...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2025
|
| Témata: | |
| On-line přístup: | https://is.muni.cz/th/bw4ql/ |
| LEADER | 04519ctm a22006137i 4500 | ||
|---|---|---|---|
| 001 | MUB01006554643 | ||
| 003 | CZ BrMU | ||
| 005 | 20251121100259.0 | ||
| 008 | 250613s2025 xr ||||| |||||||||||eng d | ||
| 035 | |a (ISMU-VSKP)310499 | ||
| 040 | |a BOD114 |b cze |d BOD018 |e rda | ||
| 072 | 7 | |a 004.4/.6 |x Programování. Software |2 Konspekt |9 23 | |
| 080 | |a 004.052.42 |2 MRF | ||
| 080 | |a 81'37 |2 MRF | ||
| 080 | |a 004.43 |2 MRF | ||
| 080 | |a 16 |2 MRF | ||
| 080 | |a 168.3 |2 MRF | ||
| 100 | 1 | |a Tušil, Jan |% UČO 410062 |* [absolvent FI MU] |4 dis | |
| 242 | 1 | 0 | |a Progress in Programming Language Semantics Frameworks |y eng |
| 245 | 1 | 0 | |a Progress in Programming Language Semantics Frameworks / |c Jan Tušil |
| 264 | 0 | |c 2025 | |
| 300 | |a 159 stran : |b ilustrace | ||
| 336 | |a text |b txt |2 rdacontent | ||
| 337 | |a bez média |b n |2 rdamedia | ||
| 338 | |a svazek |b nc |2 rdacarrier | ||
| 500 | |a Vedoucí práce: Jan Obdržálek | ||
| 502 | |a Dizertace (Ph.D.)--Masarykova univerzita, Fakulta informatiky, 2025 | ||
| 520 | 2 | |a Představa masové produkce počítačového software bez použití vysokoúrovňových programovacích jazyků je obtížná. Tyto jazyky odstiňují softwarové inženýry od detailů přítomných v moderních počítačových architekturách: instrukční sady, keše, provádění instrukcí mimo pořadí, a tak dále. Ale když se abstrahujeme od těchto detailů, co zbyde z programovacího jazyka? Když tyto "zbytky" - sémantiku daného programovacího jazyka - přesně popíšeme, důležité otázky začnou dávat smysl: otázky typu "Je tento překladač korektní?" či "Může můj program selhat?". Můžeme však jít ještě dále: s jednotným konceptem "sémantiky" sdílené mezi jazyky, vývoj programovacích jazyků se zjednodušší a zautomatizuje. Například je možné napsat interpreter nebo deduktivní verifikátor takovým způsobem, že tento je parametrický v sémantice cílového programovacího jazyka, a následně získat interpreter nebo verifikátor pro libovolný jazyk popsaný uvnitř takovéhoto frameworku téměř zadarmo. Tato práce představuje tři přísp |% cze | |
| 520 | 2 | 9 | |a One can hardly imagine large-scale production of computer software without the use of high-level programming languages. These shield software engineers from the overwhelming amount of detail present in modern computer architectures: instruction sets, caches, out-of-order execution, and so on. But when these details are abstracted, what does remain of a programming language? When the remains - a programming language’s semantics - are precisely captured, important questions such as “Is this compiler correct?” or “Can my program go wrong?” become meaningful. Furthermore, with a common notion of language semantics shared between languages, the development of programming language tools becomes easier and more automated. For example, it is possible to write an interpreter or a deductive verifier such that it is parametric in the semantics of the target language, and then obtain the interpreter or verifier almost for free for any language expressed within the framework. This thesis presents |9 eng |
| 650 | 0 | 7 | |a formální verifikace |7 ph755479 |2 czenas |
| 650 | 0 | 7 | |a sémantika |7 ph117272 |2 czenas |
| 650 | 0 | 7 | |a programovací jazyky |7 ph115890 |2 czenas |
| 650 | 0 | 7 | |a logika |7 ph122436 |2 czenas |
| 650 | 0 | 7 | |a teorie důkazu |7 ph126551 |2 czenas |
| 650 | 0 | 9 | |a formal verification |2 eczenas |
| 650 | 0 | 9 | |a semantics |2 eczenas |
| 650 | 0 | 9 | |a programming languages |2 eczenas |
| 650 | 0 | 9 | |a logic |2 eczenas |
| 650 | 0 | 9 | |a proof theory |2 eczenas |
| 655 | 7 | |a disertace |7 fd132024 |2 czenas | |
| 655 | 9 | |a dissertations |2 eczenas | |
| 658 | |a Informatika |b Technologie a metodologie počítačových systémů |c FI D-INF DIIA (DIIA) |2 CZ-BrMU | ||
| 700 | 1 | |a Obdržálek, Jan, |d 1977- |7 jx20100824012 |% UČO 1552 |4 ths | |
| 710 | 2 | |a Masarykova univerzita. |b Fakulta informatiky. |b Katedra teorie programování |4 dgg | |
| 856 | 4 | 1 | |u https://is.muni.cz/th/bw4ql/ |
| CAT | |c 20250613 |l MUB01 |h 0421 | ||
| CAT | |a HANAV |b 02 |c 20250615 |l MUB01 |h 2338 | ||
| CAT | |a POSPEL |b 02 |c 20250617 |l MUB01 |h 1013 | ||
| CAT | |a POSPEL |b 02 |c 20250617 |l MUB01 |h 1014 | ||
| CAT | |a VESELA |b 02 |c 20251120 |l MUB01 |h 1519 | ||
| CAT | |a VESELA |b 02 |c 20251121 |l MUB01 |h 1002 | ||
| 994 | - | 1 | |l MUB01 |l MUB01 |m VYSPR |1 FI |a Fakulta informatiky |2 SKLAD |b sklad |3 Diz. práce 2025 |5 42005D2796 |8 20251120 |f 72 |f Týdenní |r 20251120 |
| AVA | |a INF50 |b FI |c sklad |d Diz. práce 2025 |e available |t K dispozici |f 1 |g 0 |h N |i 0 |j SKLAD | ||