Meta tags:
Headings (most frequently used words):
2026, concur, science, 20, friday, august, 21, monday, 03, april, gandalf, interview, with, tot, award, computer, process, algebra, diary, sunday, september, thursday, may, saturday, march, 28, pages, blog, archive, about, me, notes, on, krishnendu, chatterjee, tom, henzinger, and, nir, piterman, recipients, tenure, track, position, in, at, the, gran, sasso, institute, gssi, naoki, kobayashi, recipient, test, of, time, awards, estonian, latvian, theory, days, first, call, for, papers,
Text of the page (most frequently used words):
the (294), and (161), for (85), that (81), you (49), logic (46), type (40), 2026 (33), this (33), time (30), luca (29), was (29), your (29), with (28), strategy (28), may (27), such (27), #theory (25), concur (25), paper (25), games (24), are (23), can (23), calculus (23), april (22), naoki (22), research (22), also (22), september (21), share (21), system (21), would (21), systems (21), work (20), june (19), from (19), award (19), what (19), game (19), august (18), november (18), march (18), automata (18), deadlock (18), did (18), january (17), have (17), july (16), december (16), february (16), more (16), other (16), were (15), not (15), some (15), there (15), which (15), one (15), october (14), between (14), has (13), but (13), freedom (13), atl (13), strategies (13), gandalf (12), very (12), how (12), based (12), knt (12), 2006 (11), will (11), see (11), two (11), kobayashi (11), think (11), been (11), winning (11), our (10), related (10), model (10), checking (10), any (10), developed (10), article (10), natural (10), could (10), questions (10), email (9), verification (9), first (9), main (9), science (9), these (9), good (9), methods (9), ideas (9), they (9), expressive (9), implementation (9), aceto (8), about (8), logics (8), computer (8), community (8), free (8), types (8), result (8), than (8), most (8), them (8), techniques (8), while (8), results (8), dependencies (8), express (8), multi (8), alternating (8), pinterest (7), facebook (7), blogthis (7), comments (7), posted (7), formal (7), talk (7), however (7), nir (7), researchers (7), important (7), topics (7), came (7), find (7), interesting (7), lock (7), reasoning (7), using (7), study (7), had (7), process (7), general (7), linear (7), equilibria (7), synthesis (7), days (6), direction (6), further (6), obligation (6), receive (6), capability (6), open (6), all (6), infinite (6), question (6), non (6), agent (6), their (6), event (5), papers (5), university (5), https (5), colleagues (5), year (5), krishnendu (5), new (5), tot (5), finding (5), young (5), languages (5), possible (5), future (5), agents (5), properties (5), only (5), automated (5), concurrent (5), key (5), like (5), still (5), expressiveness (5), mentioned (5), davide (5), sangiorgi (5), developments (5), three (5), power (5), those (5), fragment (5), inference (5), indeed (5), later (5), analysis (5), different (5), his (5), phd (5), full (5), graphs (5), complexity (5), algorithmic (5), logical (5), framework (5), computational (5), support (5), player (5), 2010 (4), giorgio (4), bacci (4), symposium (4), held (4), life (4), theoretical (4), well (4), both (4), committee (4), made (4), piterman (4), henzinger (4), processes (4), test (4), genai (4), directions (4), programs (4), researcher (4), working (4), rather (4), role (4), setting (4), much (4), right (4), channels (4), notions (4), useful (4), example (4), line (4), language (4), problems (4), levels (4), amongst (4), within (4), answer (4), order (4), tags (4), typed (4), lower (4), already (4), algorithm (4), used (4), extensions (4), 2004 (4), among (4), idea (4), ensure (4), italian (4), aquila (4), italy (4), competitive (4), gssi (4), delivered (4), volume (4), alternation (4), graph (4), reactive (4), concepts (4), several (4), bound (4), tom (4), behavioral (4), version (4), ltl (4), talks (4), complete (3), 2007 (3), information (3), call (3), aalborg (3), international (3), period (3), gave (3), tartu (3), structures (3), estonian (3), latvian (3), edition (3), invited (3), get (3), students (3), choice (3), thomas (3), chatterjee (3), awards (3), opportunity (3), play (3), advice (3), learn (3), carefully (3), same (3), written (3), give (3), who (3), start (3), programming (3), cost (3), lightweight (3), combining (3), coding (3), change (3), annotations (3), then (3), become (3), even (3), now (3), because (3), similar (3), naturally (3), notion (3), operation (3), guarantee (3), request (3), handle (3), influence (3), builds (3), least (3), explored (3), necessary (3), approach (3), since (3), left (3), semantic (3), thereby (3), limitations (3), control (3), chains (3), through (3), others (3), hindsight (3), contributions (3), recursion (3), progress (3), property (3), into (3), viewed (3), concurrency (3), showed (3), say (3), typical (3), fully (3), readers (3), whether (3), worth (3), hard (3), implement (3), combine (3), handled (3), its (3), point (3), form (3), 2005 (3), challenging (3), over (3), previous (3), lnkd (3), applications (3), application (3), central (3), excellent (3), postdoctoral (3), tenure (3), track (3), programme (3), include (3), areas (3), group (3), algorithms (3), software (3), vol (3), context (3), rational (3), many (3), strictly (3), behaviors (3), players (3), part (3), checks (3), always (3), strategic (3), started (3), elementary (3), matching (3), tree (3), tell (3), tool (3), behavior (3), way (3), explicit (3), objects (3), consider (3), pre (3), operators (3), defining (3), algebra (3), view (2), 2008 (2), 2009 (2), 2011 (2), 2014 (2), 2018 (2), 2025 (2), notes (2), home (2), posts (2), submit (2), elli (2), anastasiadi (2), chaired (2), denmark (2), randour (2), mons (2), seventeenth (2), estonia (2), organising (2), robert (2), tarjan (2), data (2), feature (2), countries (2), people (2), welcome (2), audience (2), roles (2), website (2), department (2), friday (2), recipients (2), selected (2), following (2), monday (2), above (2), challenges (2), changes (2), explore (2), classical (2), keen (2), design (2), precision (2), beyond (2), incorporating (2), era (2), focus (2), broadly (2), humans (2), therefore (2), program (2), minimal (2), hamin (2), jacobs (2), monitors (2), esop (2), leino (2), locks (2), protocols (2), obligations (2), capabilities (2), out (2), another (2), conventional (2), applied (2), extended (2), variables (2), found (2), shows (2), send (2), describes (2), need (2), client (2), server (2), eventually (2), after (2), subsequent (2), obtained (2), particular (2), increasing (2), make (2), practical (2), interactive (2), theorem (2), remains (2), problem (2), suggested (2), love (2), solved (2), hybrid (2), mobile (2), syntactic (2), typing (2), rules (2), ones (2), tools (2), provide (2), guide (2), capture (2), causal (2), numbers (2), called (2), termination (2), formulation (2), seminal (2), contribution (2), desirable (2), examples (2), instance (2), induced (2), achieved (2), partial (2), conceptual (2), encoding (2), functional (2), evaluation (2), does (2), stuck (2), encodability (2), possibly (2), level (2), simply (2), things (2), every (2), proposal (2), accompanied (2), improvement (2), practice (2), benefit (2), ought (2), generic (2), elena (2), giachino (2), cosimo (2), laneve (2), networks (2), technically (2), extension (2), extend (2), doing (2), benjamin (2), pierce (2), david (2), turner (2), really (2), lics (2), 1997 (2), goals (2), balance (2), expressed (2), restricted (2), pleasing (2), completely (2), giving (2), surprising (2), addressed (2), briefly (2), explain (2), appeared (2), kindly (2), agreed (2), mine (2), via (2), post (2), answers (2), below (2), hope (2), enjoy (2), reading (2), thanks (2), interview (2), apply (2), recognition (2), offers (2), quality (2), academic (2), environment (2), english (2), recognized (2), teaching (2), whose (2), gran (2), sasso (2), institute (2), position (2), unifying (2), themes (2), connects (2), studied (2), area (2), history (2), exciting (2), makes (2), difficult (2), believe (2), ever (2), field (2), seems (2), signs (2), early (2), mas (2), uptake (2), happy (2), collaboration (2), studying (2), led (2), trees (2), together (2), meeting (2), wish (2), build (2), distinction (2), done (2), mcmas (2), having (2), relevant (2), hence (2), relate (2), defined (2), anyone (2), checker (2), implementations (2), modal (2), single (2), branching (2), objectives (2), treats (2), class (2), decidability (2), fragments (2), treating (2), explicitly (2), adversarial (2), connections (2), aspects (2), imho (2), regular (2), clear (2), social (2), contributed (2), presentations (2), covered (2), ezio (2), recent (2), sarah (2), nicola (2), wheeler (2), small (2), scientific (2), diary (2), awesome, inc, theme, powered, blogger, profile, 109, 2012, 2013, 2015, 2016, 2017, 2019, 2020, 2021, 2022, 2023, 2024, blog, archive, pages, subscribe, atom, older, spread, news, mickaël, université, belgium, organised, gandalfsymposium, github, saturday, recording, kudos, latvia, note, deadlines, registration, proposing, today, www, youtube, com, watch, pfhiuexfhwg, last, public, lecture, entitled, joint, goal, let, scientists, acquainted, each, participate, intended, graduate, listeners, presenters, quoting, reykjavik, hat, tip, colleague, tarmo, uustalu, congratulations, whole, truly, wonderful, consisting, anca, muscholl, chair, javier, esparza, prakash, panangaden, announced, discussed, rapidly, changing, landscape, facing, significant, adapting, native, foundations, constrained, traditional, assumptions, verified, respect, seen, product, former, philosophy, emphasized, automation, move, dependent, aiming, situation, generate, loop, invariants, burden, writing, longer, serious, issue, aim, strong, correctness, guarantees, merely, bugs, traditionally, played, keep, automate, bug, sometimes, completeness, should, jafar, bart, 415, 441, rustan, peter, müller, jan, smans, 407, 426, morten, dahl, yunde, sun, hans, hüttel, authenticity, asymmetric, cryptographic, atva, dual, turned, contexts, adapted, security, condition, particularly, arise, ingredient, perform, succeed, successfully, mutual, exclusion, thread, acquire, acquiring, release, integrating, probably, second, inherently, incomplete, smooth, integration, proving, acm, trans, lang, syst, address, limitation, latter, discharged, resorting, checkers, provers, complementing, combination, common, structural, patterns, cases, fall, outside, reach, purely, forbids, cyclic, forbid, suffers, inherent, yuxin, deng, relations, underlie, systematic, fashion, ensuring, typability, ock, challenge, finite, representation, reason, considering, corresponds, thus, preserved, compilation, parallel, cps, style, primitives, sort, requirement, shown, original, wanted, show, retained, encoded, convincing, sufficiently, overcome, developing, inspirations, cav, although, absolutely, identifying, suggesting, initially, proof, concept, mainly, convince, works, theories, supported, guaranteeing, commendably, atsushi, igarashi, theor, comput, sci, 311, 121, 163, unbounded, pushing, feeling, purpose, easily, involved, perhaps, promising, adapt, real, kinds, beneficial, precise, set, unfortunately, investigated, deal, value, passing, ccs, achieves, trade, off, ease, implementing, associated, try, range, variation, hit, diminishing, returns, where, advance, technical, remember, correctly, during, discussions, wants, channel, exactly, once, before, initial, published, enabling, somewhat, conflicting, core, follows, replaced, enable, combined, recovering, retaining, precisely, significantly, without, elegance, earlier, linearity, popl, 1996, 358, partially, 128, 139, flow, acta, informatica, 291, 347, hich, evolved, culmination, series, development, variations, delighted, recipient, thursday, gbnzua7b, official, gycbshda, applicants, holding, procedure, pending, provided, evidence, filed, here, gnczksdn, must, submitted, pica, platform, located, mountains, welcoming, immediate, access, nature, outdoor, activities, city, positioned, reaching, rome, adriatic, coast, deadline, instruction, eligibility, equivalent, qualification, years, documented, experience, location, contract, six, appointment, details, requirements, successful, candidate, expected, establish, independent, internationally, supervise, collaborate, strengthen, attract, funding, school, advanced, studies, responsibilities, doctoral, courses, seminars, candidates, complements, expands, interdisciplinary, profiles, strongly, encouraged, top, ranked, national, excellence, artificial, intelligence, engineering, addresses, fields, robotics, human, centric, cyber, physical, internet, space, smart, cities, invites, inflow, source, broad, benefited, grounded, axiomatic, characterizations, spaces, influential, evolutionary, mechanism, relationship, lens, determinism, bounds, fundamental, remain, polynomial, parity, iii, degree, sources, randomness, shared, active, computationally, efficient, lie, under, rapid, computing, generated, needs, modern, scale, hitherto, impossible, necessarily, take, lean, proofs, state, involving, predict, place, uniquely, wouldn, saw, coming, adoption, 2000s, regularly, major, definitely, established, upper, gap, closed, proved, settled, concentrated, case, interaction, structure, means, sense, captures, interested, collaborations, stories, ages, grew, concise, pursuing, realized, meant, expert, ingredients, zero, sum, lasting, interplay, exploited, fed, directly, lines, connection, deterministic, emerged, special, classes, elegant, mind, tcs, bridging, divide, covering, subject, matter, impact, construed, reminded, typically, thought, provoking, moshe, vardi, learnt, anything, slides, book, length, treatment, supports, principle, reduce, aware, implemented, answered, incentive, follow, protocol, stability, coalitions, individuals, profitably, deviate, puts, center, continue, exploring, allow, starting, exploration, mix, might, understand, else, present, negative, interest, experimental, far, know, supporting, manipulation, words, spot, owl, basis, creating, solve, required, adopted, equilibrium, eve, michael, wooldridge, oxford, epistemic, included, alessio, lomuscio, imperial, college, london, hinting, incomparable, fixed, achieving, best, worlds, maintaining, worked, intuitively, calculi, local, transition, fixpoint, whereas, global, choices, outcomes, paths, difference, due, archival, introduced, expressing, features, named, quantify, motivation, appealing, admits, come, clean, reasonable, establishing, various, describe, sounds, extremely, followed, path, recall, realisation, until, primarily, cooperative, around, consequence, considered, nash, secure, fact, isolated, suffices, afterwards, arrived, shift, driven, asking, eureka, moment, basing, tension, stronger, formalisms, recognize, tradition, chose, exact, formalism, etl, qltl, ldl, long, readily, translated, nesting, fixpoints, coalition, quantification, define, infinitely, manner, henceforth, abbreviated, computation, reasons, attended, few, conferences, workshops, quite, exception, glad, behalf, steering, thank, putting, lovely, pleasure, visit, stamping, grounds, departments, luck, next, giovanni, scientifc, mickael, high, especially, day, references, lord, rings, featured, appearance, stages, careers, spans, told, rule, guided, explainable, testing, deep, reinforcement, learning, policies, her, approaches, hyperproperties, described, compression, focusing, search, planned, message, speakers, want, presented, dblp, short, summary, thesis, martin, zimmermann, cotumaccio, winter, bartocci, devoted, inception, participants, thoroughly, enjoyed, programmes, friends, relaxed, friendly, listening, discussing, variety, attendees, honest, prefer, taking, gatherings, big, sunday, mostly, solely, fun, stuff, mathematics, large, issues,
Text of the page (random words):
do not necessarily have to take the form of say lean proofs but they could also include state based reasoning involving automata and games it is always difficult to predict the future but finding the right place for our field in this future seems a uniquely exciting opportunity posted by luca aceto at 2 56 pm no comments email this blogthis share to x share to facebook share to pinterest monday august 03 2026 tenure track position in computer science at the gran sasso science institute gssi the gran sasso science institute gssi in l aquila italy invites applications for a full time tenure track researcher position in computer science the gssi computer science group is among the top ranked in italy and has been recognized as a national department of excellence its main areas of research include algorithms artificial intelligence formal methods and software engineering research also addresses applications in fields such as robotics human centric systems cyber physical systems the internet of things space and smart cities we welcome candidates whose research complements or expands these areas excellent theoretical applied and interdisciplinary profiles are strongly encouraged to apply the successful candidate will be expected to establish an independent and internationally recognized research programme supervise phd students collaborate with postdoctoral researchers strengthen international research networks and attract competitive research funding the gssi is a school of advanced studies teaching responsibilities will include doctoral and postdoctoral courses and seminars delivered in english key details requirements contract six year full time tenure track appointment location l aquila italy eligibility phd or equivalent qualification and at least two years of documented postdoctoral research experience language of instruction english application deadline 17 august 2026 23 59 italian time about l aquila located in the mountains of central italy l aquila offers an excellent quality of life a welcoming international academic environment and immediate access to nature and outdoor activities the city is also well positioned for reaching rome and the adriatic coast application process applications must be submitted through the pica platform https lnkd in gnczksdn applicants holding a non italian phd may apply while the italian recognition procedure is pending provided that they submit evidence that a recognition request has been filed see more here https lnkd in gycbshda official call in italian https lnkd in gbnzua7b posted by luca aceto at 10 12 pm no comments email this blogthis share to x share to facebook share to pinterest thursday may 21 2026 interview with naoki kobayashi concur 2026 tot award recipient as mentioned in a previous post naoki kobayashi will receive one of the two concur 2026 test of time awards at concur 2026 naoki has kindly agreed to answer some questions of mine on his award winning paper via email i am delighted to post his answers below and hope you ll enjoy reading them as much as i did thanks naoki luca you receive the concur tot award 2026 for your paper a new type system for deadlock free processes which appeared at concur 2006 that article is the culmination of a series of contributions you gave on the development of type systems for variations on the pi calculus that guarantee deadlock freedom could you briefly explain to our readers how you came to study the question addressed in your award winning article and how the main ideas in your concur 2006 paper evolved over time w hich of the ideas and results in your paper did you find most pleasing surprising or challenging naoki if i remember correctly the idea of using types to ensure deadlock freedom came up during discussions on the linear pi calculus with benjamin pierce and david turner 1 indeed if one wants to ensure that a channel is really used exactly once one also has to ensure that the process does not get stuck before using it an initial result on type systems for deadlock freedom was published in lics 1997 2 after that the type system was extended in two directions enabling automated type inference and increasing expressiveness these were somewhat conflicting goals and the concur 2006 paper achieved a balance between them the core idea was as follows to ensure deadlock freedom it is necessary to control dependencies among different channels in 2 such dependencies were expressed using time tags and a possibly infinite partial order on them the time tags were later replaced by natural numbers called capability and obligation levels to enable automated inference 3 but at the cost of expressive power the concur 2006 paper combined a restricted form of time tags with capability and obligation levels thereby recovering much of the expressive power while retaining automated inference what i found most pleasing was precisely this balance the paper showed that one could make the type system significantly more practical without completely giving up the conceptual elegance and expressiveness of the earlier formulation 1 naoki kobayashi benjamin c pierce david n turner linearity and the pi calculus popl 1996 358 37 2 naoki kobayashi a partially deadlock free typed process calculus lics 1997 128 139 3 naoki kobayashi type based information flow analysis for the pi calculus acta informatica 42 4 5 291 347 2005 luca the contribution in your article achieves a good trade off between expressiveness of the type system and ease of implementing its associated type inference algorithm did you or any other researcher try to extend the range of examples that could be handled by a variation on your type system do you think that it would be worth doing so or have we hit the point of diminishing returns where any advance would be very technical and hard to implement naoki with elena giachino and cosimo laneve 4 i indeed investigated such an extension the system developed there can deal with infinite chains of dependencies more general than those handled in the concur 2006 paper it was however developed for value passing ccs rather than the pi calculus incorporating the idea of 4 into the pi calculus setting remains future work another possible direction would be to combine the approach with generic types 5 which can capture precise dependencies among a set of channels unfortunately i did not have time to fully explore this direction as for whether it is worth pushing this line further my feeling is that further general purpose extensions may easily become technically involved and hard to implement perhaps a more promising direction would be to adapt the type system to real concurrent languages such as go and then see what kinds of extensions are most beneficial in practice 4 elena giachino naoki kobayashi cosimo laneve deadlock analysis of unbounded process networks concur 2014 63 77 5 atsushi igarashi naoki kobayashi a generic type system for the pi calculus theor comput sci 311 1 3 121 163 2004 luca commendably you supported the theoretical developments in your article with an implementation in typical what role did the implementation work play in your research on type systems guaranteeing deadlock freedom did the theoretical developments benefit from the implementation do you think that every proposal for a type system for some language ought to be accompanied by an implementation naoki typical was initially developed as a proof of concept for the type inference algorithm of 3 at that time the theory had already been fully developed and the implementation was mainly used to convince readers that the algorithm indeed works in practice in later extensions of typical for the concur 2006 paper and the work of 6 the implementation was also useful for checking the theories i think it is desirable for every type system proposal to be accompanied by an implementation although i would not say that it is absolutely necessary an implementation is useful not only for checking the theory but also for identifying limitations of the theory and suggesting possible directions for improvement 6 naoki kobayashi davide sangiorgi a hybrid type system for lock freedom of mobile processes cav 2008 80 93 luca in your paper you showed amongst other things that the simply typed λ calculus with recursion could be encoded in the deadlock free fragment of your calculus what role did this result play in convincing you that your type system was sufficiently expressive what were the main challenges that you had to overcome in developing that encoding and what were the main inspirations for that result naoki the encodability of the simply typed λ calculus with recursion in the deadlock free fragment was a sort of minimal requirement for expressiveness since that property had already been shown for the original deadlock free type system 2 i wanted to show that a similar level of expressive power was retained in the concur 2006 type system there was also a more conceptual reason for considering such an encoding deadlock freedom corresponds to the progress property of well typed functional programs evaluation does not get stuck thus the encodability result shows that this progress property can be preserved by compilation from possibly parallel functional programs into the pi calculus which may be viewed as a cps style lower level language with concurrency primitives the main challenge was how to give a finite representation within the type system of the infinite chains of causal dependencies induced by recursion as mentioned in the answer to the first question we achieved this by combining the ideas of capability obligation levels from 3 with a partial order on time tags from 2 luca your article gave a seminal contribution to the study of type systems for the pi calculus that guarantee some desirable properties other examples of such contributions are for instance your paper with davide sangiorgi on a type system for l ock freedom or the paper by yuxin deng and davide sangiorgi on ensuring termination by typability amongst others in hindsight are there any relations amongst those contributions or ideas that underlie them and that can guide further developments in a systematic fashion naoki all three type systems you mentioned are related in that they control causal dependencies using natural numbers called levels the type system for deadlock freedom forbids cyclic dependencies while the type systems for lock freedom and termination forbid infinite chains of dependencies the formulation of such reasoning through types however suffers from inherent limitations in expressive power to address this limitation my paper with davide sangiorgi 7 suggested a new direction combining syntactic typing rules with semantic ones the latter can be discharged by resorting to model checkers interactive theorem provers or other verification tools thereby complementing the limitations of type systems i think this combination of type based reasoning and semantic verification may provide a useful guide for further developments types can capture common structural patterns while semantic methods can handle cases that fall outside the reach of purely syntactic typing rules 7 naoki kobayashi davide sangiorgi a hybrid type system for lock freedom of mobile processes acm trans program lang syst 32 5 16 1 16 49 2010 luca are there any problems that you left open in your award winning article that you d still love to see solved naoki i would still like to see at least two directions explored further first increasing the expressiveness of the type system by integrating the ideas of 4 and 5 mentioned above would probably be necessary to make the approach practical second since the type based approach is inherently incomplete finding a smooth integration with other methods such as model checking and interactive theorem proving remains an important open problem as suggested in 6 luca how did the results and the techniques you developed in your award winning paper influence your subsequent research is there any result obtained by other researchers that builds on or is related to your work and that you like in particular naoki a key ingredient of our type systems for deadlock freedom is the notion of obligations and capabilities an obligation of a send or receive operation describes the need to perform that operation while a capability describes a guarantee that the operation can succeed for example in a client server model a client has the capability to send a request successfully while a server has an obligation to receive and handle the request in lock based mutual exclusion a thread has the capability to eventually acquire a lock and after acquiring the lock it has an obligation to eventually release the lock these dual notions of obligations and capabilities turned out to be useful in other contexts for example we adapted them for automated verification of security protocols 8 another line of work developed related ideas for more conventional concurrent programming languages leino et al 9 applied related techniques to deadlock freedom of channels and locks and this line was further extended to monitors and condition variables by hamin and jacobs 10 i found this line of work particularly interesting because it shows that similar ideas arise naturally also in a more conventional programming language setting 8 morten dahl naoki kobayashi yunde sun hans hüttel type based automated verification of authenticity in asymmetric cryptographic protocols atva 2011 75 89 9 k rustan m leino peter müller jan smans deadlock free channels and locks esop 2010 407 426 10 jafar hamin bart jacobs deadlock free monitors esop 2018 415 441 luca what are the research topics related to type systems that you find most interesting right now what role do you think type systems will or should have if any in the era of coding agents based on genai naoki i think genai may change not only type systems but also the focus of formal methods more broadly traditionally programs have been written by humans and therefore lightweight formal methods have played an important role in that setting it was important to keep program annotations minimal and to automate verification or bug finding as much as possible even if this sometimes came at the cost of precision or completeness in the era of genai based coding agents however the situation may change if coding agents can also generate annotations such as types and loop invariants then the burden of writing annotations may no longer be such a serious issue as a result verification methods that aim at strong correctness guarantees rather than merely finding bugs or checking lightweight properties may become more important in this respect the concur 2006 type system can be seen as a product of the former design philosophy it emphasized automation at some cost in precision a possible future direction would be to move beyond such lightweight type systems by incorporating dependent types or combining type system...
|
