BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Trifon Trifonov

Trifon Trifonov appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
astro-ph.EPastro-ph.SRastro-ph.IMastro-ph.COastro-ph.GAastro-ph.HELogic in Computer Science

Catalog footprint

What is connected

16works
7topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

16 published item(s)

preprint2022arXiv

A low-eccentricity migration pathway for a 13-h-period Earth analogue in a four-planet system

It is commonly accepted that exoplanets with orbital periods shorter than 1 day, also known as ultra-short period (USP) planets, formed further out within their natal protoplanetary disk, before migrating to their current-day orbits via dynamical interactions. One of the most accepted theories suggests a violent scenario involving high-eccentricity migration followed by tidal circularization. Here, we present the discovery of a four planet system orbiting the bright (V=10.5) K6 dwarf star TOI-500. The innermost planet is a transiting, Earth-sized USP planet with an orbital period of $\sim$ 13 hours, a mass of 1.42 $\pm$ 0.18 M$_{\oplus}$, a radius of $1.166^{0.061}_{-0.058}$ R$_{\oplus}$, and a mean density of 4.89$^{+1.03}_{-0.88}$ gcm$^{-3}$. Via Doppler spectroscopy, we discovered that the system hosts three outer planets on nearly circular orbits with periods of 6.6, 26.2, and 61.3d and minimum masses of 5.03 $\pm$ 0.41 M$_{\oplus}$, 33.12 $\pm$ 0.88 M$_{\oplus}$ and 15.05$^{+1.12}_{-1.11}$ M$_{\oplus}$, respectively. The presence of both a USP planet and a low-mass object on a 6.6-day orbit indicates that the architecture of this system can be explained via a scenario in which the planets started on low-eccentricity orbits, then moved inwards through a quasi-static secular migration. Our numerical simulations show that this migration channel can bring TOI-500 b to its current location in 2 Gyrs, starting from an initial orbit of 0.02au. TOI-500 is the first four planet system known to host a USP Earth analog whose current architecture can be explained via a non-violent migration scenario.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

A transiting, temperate mini-Neptune orbiting the M dwarf TOI-1759 unveiled by TESS

We report the discovery and characterization of TOI-1759~b, a temperate (400 K) sub-Neptune-sized exoplanet orbiting the M~dwarf TOI-1759 (TIC 408636441). TOI-1759 b was observed by TESS to transit on sectors 16, 17 and 24, with only one transit observed per sector, creating an ambiguity on the orbital period of the planet candidate. Ground-based photometric observations, combined with radial-velocity measurements obtained with the CARMENES spectrograph, confirm an actual period of $18.85019 \pm 0.00014$ d. A joint analysis of all available photometry and radial velocities reveal a radius of $3.17 \pm 0.10\,R_\oplus$ and a mass of $10.8 \pm 1.5\,M_\oplus$. Combining this with the stellar properties derived for TOI-1759 ($R_\star = 0.597 \pm 0.015\,R_\odot$; $M_\star = 0.606 \pm 0.020\,M_\odot$; $T_{\textrm{eff}} = 4065 \pm 51$ K), we compute a transmission spectroscopic metric (TSM) value of over 80 for the planet, making it a good target for transmission spectroscopy studies. TOI-1759 b is among the top five temperate, small exoplanets ($T_\textrm{eq} < 500$ K, $R_p < 4 \,R_\oplus$) with the highest TSM discovered to date. Two additional signals with periods of 80 d and $>$ 200 d seem to be present in our radial velocities. While our data suggest both could arise from stellar activity, the later signal's source and periodicity are hard to pinpoint given the $\sim 200$ d baseline of our radial-velocity campaign with CARMENES. Longer baseline radial-velocity campaigns should be performed in order to unveil the true nature of this long period signal.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Dynamical architecture of the HD 107148 system

We present an independent Doppler validation and dynamical orbital analysis of the two-planet system HD 107148, which was recently announced in Rosenthal et al. (2021). Our detailed analyses are based on literature HIRES data and newly obtained HARPS and CARMENES radial velocity (RV) measurements as part of our survey in search for additional planets around single planet systems. We perform a periodogram analysis of the available HIRES and HARPS precise RVs and stellar activity indicators. We do not find any apparent correlation between the RV measurements and the stellar activity indicators, thus linking the two strong periodicities to a moderately compact multiple-planet system. We carry out orbital fitting analysis by testing various one- and two-planet orbital configurations and studying the posterior probability distribution of the fitted parameters. Our results solidify the existence of a Saturn-mass planet (HD 107148 b, discovered first) with a period $P_b\sim77.2$ d, and a second, eccentric ($e_c \sim$ 0.4), Neptune-mass exoplanet (HD 107148 c), with an orbital period of $P_c\sim18.3$ d. Finally, we investigate the two-planet system's long-term stability and overall orbital dynamics with the posterior distribution of our preferred orbital configuration. Our N-body stability simulations show that the system is long-term stable and exhibits large secular osculations in eccentricity but in no particular mean-motion resonance configuration. The HD 107148 system, consisting of a Solar-type main sequence star with two giant planets in a rare configuration, features a common proper motion white dwarf companion and is, therefore, a valuable target for understanding the formation and evolution of planetary systems.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

A photospheric and chromospheric activity analysis of the quiescent retrograde-planet host $ν$ Octantis A

The single-lined spectroscopic binary $ν$ Octantis provided evidence of the first conjectured circumstellar planet demanding an orbit retrograde to the stellar orbits. The planet-like behaviour is now based on 1437 radial velocities (RVs) acquired from 2001 to 2013. $ν$ Oct's semimajor axis is only 2.6 AU with the candidate planet orbiting $ν$ Oct A about midway between. These details seriously challenge our understanding of planet formation and our decisive modelling of orbit reconfiguration and stability scenarios. However, all non-planetary explanations are also inconsistent with numerous qualitative and quantitative tests including previous spectroscopic studies of bisectors and line-depth ratios, photometry from Hipparcos and the more recent space missions TESS and GAIA (whose increased parallax classifies $ν$ Oct A closer still to a subgiant ~ K1 IV). We conducted the first large survey of $ν$ Oct A's chromosphere: 198 Ca II H-line and 1160 H $α$ indices using spectra from a previous RV campaign (2009-2013). We also acquired 135 spectra (2018-2020) primarily used for additional line-depth ratios, which are extremely sensitive to the photosphere's temperature. We found no significant RV-correlated variability. Our line-depth ratios indicate temperature variations of only $\pm$ 4 K, as achieved previously. Our atypical Ca II analysis models the indices in terms of S/N and includes covariance significantly in their errors. The H $α$ indices have a quasi-periodic variability which we demonstrate is due to telluric lines. Our new evidence provides further multiple arguments realistically only in favor of the planet.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

Precise transit and radial-velocity characterization of a resonant pair: a warm Jupiter TOI-216c and eccentric warm Neptune TOI-216b

TOI-216 hosts a pair of warm, large exoplanets discovered by the TESS Mission. These planets were found to be in or near the 2:1 resonance, and both of them exhibit transit timing variations (TTVs). Precise characterization of the planets' masses and radii, orbital properties, and resonant behavior can test theories for the origins of planets orbiting close to their stars. Previous characterization of the system using the first six sectors of TESS data suffered from a degeneracy between planet mass and orbital eccentricity. Radial velocity measurements using HARPS, FEROS, and PFS break that degeneracy, and an expanded TTV baseline from TESS and an ongoing ground-based transit observing campaign increase the precision of the mass and eccentricity measurements. We determine that TOI-216c is a warm Jupiter, TOI-216b is an eccentric warm Neptune, and that they librate in the 2:1 resonance with a moderate libration amplitude of 60 +/- 2 degrees; small but significant free eccentricity of 0.0222 +0.0005/-0.0003 for TOI-216b; and small but significant mutual inclination of 1.2-3.9 degrees (95% confidence interval). The libration amplitude, free eccentricity, and mutual inclination imply a disturbance of TOI-216b before or after resonance capture, perhaps by an undetected third planet.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

TOI-1842b: A Transiting Warm Saturn Undergoing Re-Inflation around an Evolving Subgiant

The imminent launch of space telescopes designed to probe the atmospheres of exoplanets has prompted new efforts to prioritise the thousands of transiting planet candidates for follow-up characterisation. We report the detection and confirmation of TOI-1842b, a warm Saturn identified by TESS and confirmed with ground-based observations from Minerva-Australis, NRES, and the Las Cumbres Observatory Global Telescope. This planet has a radius of $1.04^{+0.06}_{-0.05}\,R_{Jup}$, a mass of $0.214^{+0.040}_{-0.038}\,M_{Jup}$, an orbital period of $9.5739^{+0.0002}_{-0.0001}$ days, and an extremely low density ($ρ$=0.252$\pm$0.091 g cm$^{-3}$). TOI-1842b has among the best known combinations of large atmospheric scale height (893 km) and host-star brightness ($J=8.747$ mag), making it an attractive target for atmospheric characterisation. As the host star is beginning to evolve off the main sequence, TOI-1842b presents an excellent opportunity to test models of gas giant re-inflation. The primary transit duration of only 4.3 hours also makes TOI-1842b an easily-schedulable target for further ground-based atmospheric characterisation.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

A public HARPS radial velocity database corrected for systematic errors

Context. The HARPS spectrograph provides state-of-the-art stellar radial velocity (RV) measurements with a precision down to 1 m/s. The spectra are extracted with a dedicated data-reduction software (DRS) and the RVs are computed by CCF with a numerical mask. Aims. The aim of this study is three-fold: (i) Create easy access to the public HARPS RV data set. (ii) Apply the new public SERVAL pipeline to the spectra, and produce a more precise RV data set. (iii) Check whether the precision of the RVs can be further improved by correcting for small nightly systematic effects. Methods. For each star observed with HARPS, we downloaded the publicly available spectra from the ESO archive and recomputed the RVs with SERVAL. We then computed nightly zero points (NZPs) by averaging the RVs of quiet stars. Results. Analysing the RVs of the most RV-quiet stars, whose RV scatter is < 5 m/s, we find that SERVAL RVs are on average more precise than DRS RVs by a few percent. We find three significant systematic effects, whose magnitude is independent of the software used for the RV derivation: (i) stochastic variations with a magnitude of 1 m/s; (ii) long-term variations, with a magnitude of 1 m/s and a typical timescale of a few weeks; and (iii) 20-30 NZPs significantly deviating by a few m/s. In addition, we find small (< 1 m/s) but significant intra-night drifts in DRS RVs before the 2015 intervention, and in SERVAL RVs after it. We confirm that the fibre exchange in 2015 caused a discontinuous RV jump, which strongly depends on the spectral type of the observed star: from 14 m/s for late F-type stars, to -3 m/s for M dwarfs. Conclusions. Our NZP-corrected SERVAL RVs can be retrieved from a user-friendly, public database. It provides more than 212 000 RVs for about 3000 stars along with many auxiliary information, NZP corrections, various activity indices, and DRS-CCF products.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

TOI-1338: TESS' First Transiting Circumbinary Planet

We report the detection of the first circumbinary planet found by TESS. The target, a known eclipsing binary, was observed in sectors 1 through 12 at 30-minute cadence and in sectors 4 through 12 at two-minute cadence. It consists of two stars with masses of 1.1 MSun and 0.3 MSun on a slightly eccentric (0.16), 14.6-day orbit, producing prominent primary eclipses and shallow secondary eclipses. The planet has a radius of ~6.9 REarth and was observed to make three transits across the primary star of roughly equal depths (~0.2%) but different durations -- a common signature of transiting circumbinary planets. Its orbit is nearly circular (e ~ 0.09) with an orbital period of 95.2 days. The orbital planes of the binary and the planet are aligned to within ~1 degree. To obtain a complete solution for the system, we combined the TESS photometry with existing ground-based radial-velocity observations in a numerical photometric-dynamical model. The system demonstrates the discovery potential of TESS for circumbinary planets, and provides further understanding of the formation and evolution of planets orbiting close binary stars.

0 citations0 reviewsNo code linkedOpen access
preprint2019arXiv

TOI-677 b: A Warm Jupiter (P=11.2d) on an eccentric orbit transiting a late F-type star

We report the discovery of TOI-677 b, first identified as a candidate in light curves obtained within Sectors 9 and 10 of the Transiting Exoplanet Survey Satellite (TESS) mission and confirmed with radial velocities. TOI-677 b has a mass of M_p = 1.236$^{+0.069}_{-0.067}$ M_J, a radius of R_p = 1.170 +- 0.03 R_J,and orbits its bright host star (V=9.8 mag) with an orbital period of 11.23660 +- 0.00011 d, on an eccentric orbit with e = 0.435 +- 0.024. The host star has a mass of M_* = 1.181 +- 0.058 M_sun, a radius of R_* = 1.28 +- 0.03 R_sun, an age of 2.92$^{+0.80}_{-0.73}$ Gyr and solar metallicity, properties consistent with a main sequence late F star with T_eff = 6295 +- 77 K. We find evidence in the radial velocity measurements of a secondary long term signal which could be due to an outer companion. The TOI-677 b system is a well suited target for Rossiter-Mclaughlin observations that can constrain migration mechanisms of close-in giant planets.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Precise radial velocities of giant stars IX. HD 59686 Ab: a massive circumstellar planet orbiting a giant star in a ~13.6 au eccentric binary system

Context: For over 12 yr, we have carried out a precise radial velocity survey of a sample of 373 G and K giant stars using the Hamilton Échelle Spectrograph at Lick Observatory. There are, among others, a number of multiple planetary systems in our sample as well as several planetary candidates in stellar binaries. Aims: We aim at detecting and characterizing substellar+stellar companions to the giant star HD 59686 A (HR 2877, HIP 36616). Methods: We obtained high precision radial velocity (RV) measurements of the star HD 59686 A. By fitting a Keplerian model to the periodic changes in the RVs, we can assess the nature of companions in the system. In order to discriminate between RV variations due to non-radial pulsation or stellar spots we used infrared RVs taken with the CRIRES spectrograph at the Very Large Telescope. Additionally, to further characterize the system, we obtain high-resolution images with LMIRCam at the Large Binocular Telescope. Results: We report the likely discovery of a giant planet with a mass of $m_{p}~\sin i=6.92_{-0.24}^{+0.18}~M_{Jup}$ orbiting at $a_{p}=1.0860_{-0.0007}^{+0.0006}$ au from the giant star HD 59686 A. Besides the planetary signal, we discover an eccentric ($e_{B}=0.729_{-0.003}^{+0.004}$) binary companion with a mass of $m_{B}~\sin i=0.5296_{-0.0008}^{+0.0011}~M_{Sun}$ orbiting at a semi-major axis of just $a_{B}=13.56_{-0.14}^{+0.18}$ au. Conclusions: The existence of the planet HD 59686 Ab in a tight eccentric binary system severely challenges standard giant planet formation theories and requires substantial improvements to such theories in tight binaries. Otherwise, alternative planet formation scenarios such as second generation planets or dynamical interactions in an early phase of the system's lifetime should be seriously considered in order to better understand the origin of this enigmatic planet.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Disentangling 2:1 resonant radial velocity orbits from eccentric ones and a case study for HD 27894

In radial velocity observations, a pair of extrasolar planets near a 2:1 orbital resonance can be misinterpreted as a single eccentric planet, if data are sparse and measurement precision insufficient to distinguish between these models. We determine the fraction of alleged single-planet RV detected systems for which a 2:1 resonant pair of planets is also a viable model and address the question of how the models can be disentangled. By simulation we quantified the mismatch arising from applying the wrong model. Model alternatives are illustrated using the supposed single-planet system HD 27894 for which we also study the dynamical stability of near-2:1 resonant solutions. From the data scatter around the fitted single-planet Keplerians, we find that for $74\% $ of the $254$ putative single-planet systems, a 2:1 resonant pair cannot be excluded as a viable model, since the error due to the wrong model is smaller than the scatter. For $187$ stars $χ^2$-probabilities can be used to reject the Keplerian models with a confidence of $95\% $ for $54\% $ of the stars and with $99.9\% $ for $39\% $ of the stars. For HD 27894 a considerable fit improvement is obtained when adding a low-mass planet near half the orbital period of the known Jovian planet. Dynamical analysis demonstrates that this system is stable when both planets are initially placed on circular orbits. For fully Keplerian orbits a stable system is only obtained if the eccentricity of the inner planet is constrained to $<0.3$. A large part of the allegedly RV detected single-planet systems should be scrutinized in order to determine the fraction of systems containing near-2:1 resonant pairs of planets. Knowing the abundance of such systems will allow us to revise the eccentricity distribution for extrasolar planets and provide direct constraints for planetary system formation.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Precise radial velocities of giant stars VIII. Testing for the presence of planets with CRIRES Infrared Radial Velocities

We have been monitoring 373 very bright (V < 6 mag) G and K giants with high precision optical Doppler spectroscopy for more than a decade at Lick Observatory. Our goal was to discover planetary companions around those stars and to better understand planet formation and evolution around intermediate-mass stars. However, in principle, long-term, g-mode nonradial stellar pulsations or rotating stellar features, such as spots, could effectively mimic a planetary signal in the radial velocity data. Our goal is to compare optical and infrared radial velocities for those stars with periodic radial velocity patterns and to test for consistency of their fitted radial velocity semiamplitudes. Thereby, we distinguish processes intrinsic to the star from orbiting companions as reason for the radial velocity periodicity observed in the optical. Stellar spectra with high spectral resolution have been taken in the H-band with the CRIRES near-infrared spectrograph at ESO's VLT for 20 stars of our Lick survey. Radial velocities are derived using many deep and stable telluric CO2 lines for precise wavelength calibration. We find that the optical and near-infrared radial velocities of the giant stars in our sample are consistent. We present detailed results for eight stars in our sample previously reported to have planets or brown dwarf companions. All eight stars passed the infrared test. We conclude that the planet hypothesis provides the best explanation for the periodic radial velocity patterns observed for these giant stars.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Precise radial velocities of giant stars VI. A possible 2:1 resonant planet pair around the K giant star $η$ Cet

We report the discovery of a new planetary system around the K giant $η$ Cet (HIP 5364, HD 6805) based on 118 high-precision optical radial velocities taken at Lick Observatory since July 2000. Since October 2011 an additional nine near-infrared Doppler measurements have been taken using the ESO CRIRES spectrograph (VLT, UT1). The visible data set shows two clear periodicities. Although we cannot completely rule out that the shorter period is due to rotational modulation of stellar features, the infrared data show the same variations as in the optical, which strongly supports that the variations are caused by two planets. Assuming the mass of $η$ Cet to be 1.7 $M_\odot$, the best edge-on coplanar dynamical fit to the data is consistent with two massive planets ($m_b\sin i$ = 2.6 $\pm$ 0.2 $M_{\mathrm{Jup}}$, $m_c\sin i$ = 3.3 $\pm$ 0.2 $M_{\mathrm{Jup}}$), with periods of $P_b$ = 407 $\pm$ 3 days and $P_c$ = 740 $\pm$ 5 days and eccentricities of $e_b$ = 0.12 $\pm$ 0.05 and $e_c$ = 0.08 $\pm$ 0.03. We tested a wide variety of edge-on coplanar and inclined planetary configurations for stability, which agree with the derived radial velocities. We find that in certain coplanar orbital configurations with moderate $e_b$ eccentricity, the planets can be effectively trapped in an anti-aligned 2:1 mean motion resonance. A much larger non-resonant stable region exists in low-eccentricity parameter space, although it appears to be much farther from the best fit than the 2:1 resonant region. In all other cases, the system is categorized as unstable or chaotic. Another conclusion from the coplanar inclined dynamical test is that the planets can be at most a factor of $\sim$ 1.4 more massive than their suggested minimum masses. This stability constraint on the inclination excludes the possibility of two brown dwarfs, and strongly favors a planetary system.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Precise Radial Velocities of Giant Stars VII. Occurrence Rate of Giant Extrasolar Planets as a Function of Mass and Metallicity

(abridged) We have obtained precise radial velocities for a sample of 373 G and K type giants at Lick Observatory regularly over more than 12 years. Planets have been identified around 15 giant stars; an additional 20 giant stars host planet candidates. We investigate the occurrence rate of substellar companions around giant stars as a function of stellar mass and metallicity. We probe the stellar mass range from about 1 to beyond 3 M_Sun, which is not being explored by main-sequence samples. We fit the giant planet occurrence rate as a function of stellar mass and metallicity with a Gaussian and an exponential distribution, respectively. We find strong evidence for a planet-metallicity correlation among the secure planet hosts of our giant star sample, in agreement with the one for main-sequence stars. However, the planet-metallicity correlation is absent for our sample of planet candidates, raising the suspicion that a good fraction of them might indeed not be planets. Consistent with the results obtained by Johnson for subgiants, the giant planet occurrence rate increases in the stellar mass interval from 1 to 1.9 M_Sun. However, there is a maximum at a stellar mass of 1.9 +0.1/-0.5 M_Sun, and the occurrence rate drops rapidly for masses larger than 2.5-3.0 M_Sun. We do not find any planets around stars more massive than 2.7 M_Sun, although there are 113 stars with masses between 2.7 and 5 M_Sun in our sample (corresponding to a giant planet occurrence rate < 1.6% at 68.3% confidence in that stellar mass bin). We also show that this result is not a selection effect related to the planet detectability being a function of the stellar mass. We conclude that giant planet formation or inward migration is suppressed around higher mass stars, possibly because of faster disk depletion coupled with a longer migration timescale.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

4MOST - 4-metre Multi-Object Spectroscopic Telescope

The 4MOST consortium is currently halfway through a Conceptual Design study for ESO with the aim to develop a wide-field (>3 square degree, goal >5 square degree), high-multiplex (>1500 fibres, goal 3000 fibres) spectroscopic survey facility for an ESO 4m-class telescope (VISTA). 4MOST will run permanently on the telescope to perform a 5 year public survey yielding more than 20 million spectra at resolution R~5000 (λ=390-1000 nm) and more than 2 million spectra at R~20,000 (395-456.5 nm & 587-673 nm). The 4MOST design is especially intended to complement three key all-sky, space-based observatories of prime European interest: Gaia, eROSITA and Euclid. Initial design and performance estimates for the wide-field corrector concepts are presented. We consider two fibre positioner concepts, a well-known Phi-Theta system and a new R-Theta concept with a large patrol area. The spectrographs are fixed configuration two-arm spectrographs, with dedicated spectrographs for the high- and low-resolution. A full facility simulator is being developed to guide trade-off decisions regarding the optimal field-of-view, number of fibres needed, and the relative fraction of high-to-low resolution fibres. Mock catalogues with template spectra from seven Design Reference Surveys are simulated to verify the science requirements of 4MOST. The 4MOST consortium aims to deliver the full 4MOST facility by the end of 2018 and start delivering high-level data products for both consortium and ESO community targets a year later with yearly increments.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Dialectica Interpretation with Marked Counterexamples

Goedel's functional "Dialectica" interpretation can be used to extract functional programs from non-constructive proofs in arithmetic by employing two sorts of higher-order witnessing terms: positive realisers and negative counterexamples. In the original interpretation decidability of atoms is required to compute the correct counterexample from a set of candidates. When combined with recursion, this choice needs to be made for every step in the extracted program, however, in some special cases the decision on negative witnesses can be calculated only once. We present a variant of the interpretation in which the time complexity of extracted programs can be improved by marking the chosen witness and thus avoiding recomputation. The achieved effect is similar to using an abortive control operator to interpret computational content of non-constructive principles.

0 citations0 reviewsNo code linkedOpen access